------------------------------------------------------------------------
-- Surjections
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

module Function.Surjection where

open import Level
open import Function.Equality as F
  using (_⟶_) renaming (_∘_ to _⟪∘⟫_)
open import Function.Equivalence using (Equivalent)
open import Function.Injection           hiding (id; _∘_)
open import Function.LeftInverse as Left hiding (id; _∘_)
open import Data.Product
open import Relation.Binary

-- Surjective functions.

record Surjective {f₁ f₂ t₁ t₂}
                  {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
                  (to : From ⟶ To) :
                  Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  field
    from             : To ⟶ From
    right-inverse-of : from RightInverseOf to

  equivalent : Equivalent From To
  equivalent = record
    { to   = to
    ; from = from
    }

-- The set of all surjections between two setoids.

record Surjection {f₁ f₂ t₁ t₂}
                  (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
                  Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  field
    to         : From ⟶ To
    surjective : Surjective to

  open Surjective surjective public

  right-inverse : RightInverse From To
  right-inverse = record
    { to              = from
    ; from            = to
    ; left-inverse-of = right-inverse-of
    }

  injective : Injective from
  injective = LeftInverse.injective right-inverse

  injection : Injection To From
  injection = LeftInverse.injection right-inverse

-- Identity and composition.

id : ∀ {s₁ s₂} {S : Setoid s₁ s₂} → Surjection S S
id {S = S} = record
  { to         = F.id
  ; surjective = record
    { from             = LeftInverse.to              id′
    ; right-inverse-of = LeftInverse.left-inverse-of id′
    }
  } where id′ = Left.id {S = S}

infixr  _∘_

_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂}
        {F : Setoid f₁ f₂} {M : Setoid m₁ m₂} {T : Setoid t₁ t₂} →
      Surjection M T → Surjection F M → Surjection F T
f ∘ g = record
  { to         = to f ⟪∘⟫ to g
  ; surjective = record
    { from             = LeftInverse.to              g∘f
    ; right-inverse-of = LeftInverse.left-inverse-of g∘f
    }
  }
  where
  open Surjection
  g∘f = Left._∘_ (right-inverse g) (right-inverse f)