module Sets where

open import AlgebraicSignature public
open import Colimit public
open import InitialAlgebra public
open import Prelude public
open import Size
open import SizedFunctor
open import WISC

----------------------------------------------------------------------
-- The category of sets and functions
----------------------------------------------------------------------
instance
  CATSet : CAT Set
  _⟶_    {{CATSet}} A B = A → B
  ide    {{CATSet}} _   = id
  _∙_    {{CATSet}} g f = g ∘ f
  ide∙   {{CATSet}}     = refl
  ∙ide   {{CATSet}}     = refl
  ∙assoc {{CATSet}}     = refl

----------------------------------------------------------------------
-- Colimits in the category of sets
-- of diagrams on thin semi categories
----------------------------------------------------------------------
instance
  CocompleteSet : Cocomplete Set
  CocompleteSet = record
    { colim    = setcolim
    ; inc      = λ _ x d → [ x , d ]/ _
    ; cocone   = λ _ {i} j → funext λ d → quot.eq _ (mksetrel i j d)
    ; lift     = λ _ f φ → quot.lift
      (λ{(i , d) → f i d})
      (λ{(mksetrel _ j d) → ap (case d) (φ j)})
    ; liftinc  = λ _ _ _ _ → refl
    ; liftuniq =
        λ _ _ _ ψ → funext \ z → match (quot.surjectionmk _ z) \ where
          (∃i (i , d) refl) → ap (case d) (ψ i)
    }
    module _ where
    setcolim :
      {κ : Set}
      {{_ : Thin κ}}
      → --------------
      Diag κ Set → Set
    setcolim {κ} D = (∑ κ (V D)) / setrel
      module _ where
      data setrel : (_ _ : ∑ κ (V D)) → Prop where
        mksetrel :
          (i j : κ)
          {{_ : j <ᵇ i}}
          (d : V D j)
          → ----------------------------
          setrel (j , d) (i , E D i j d)

----------------------------------------------------------------------
-- Colimits in the category of sets
-- of diagrams on a size
----------------------------------------------------------------------
colimsize :
  {κ : Set}
  {{_ : Size κ}}
  (D  D' : Diag κ Set)
  (_ : D ≡ D')
  (i i' : κ)
  (d : V D i)
  (d' : V D' i')
  (_ : inc D i d ≣ inc D' i' d')
  → ---------------------------------------
  ∃ j ∶ κ , ⋀ p ∶ i <ᵇ j , ⋀ p' ∶ i' <ᵇ j ,
    (E D j i {{p}} d ≣ E D' j i' {{p'}} d')
colimsize {κ} D _ refl _ _ _ _ e =
  quot-eff R S R⊆S Srefl Ssymm Strans e
  where
  ΣD : Set
  ΣD = ∑ i ∶ κ , V D i

  R : ΣD → ΣD → Prop
  R = setrel D

  S : ΣD → ΣD → Prop
  S (i , d) (i' , d') =
    ∃ j ∶ κ , ⋀ p ∶ i <ᵇ j , ⋀ p' ∶ i' <ᵇ j ,
      (E D j i {{p}} d ≡ E D j i' {{p'}} d')

  R⊆S : ∀{z z'} → R z z' → S z z'
  R⊆S (mksetrel i j d) =
    ∃i k (⋀i j<ᵇk (⋀i <ᵇ↑ˢ (ap (case d) (symm (E∙E D k i {{<ᵇ↑ˢ}} j)))))
    where
    k : κ
    k = ↑ˢ i
    j<ᵇk : j <ᵇ k
    j<ᵇk = <ᵇ<ᵇ {{q = <ᵇ↑ˢ}}

  Srefl : ∀{z z'} → z ≡ z' → S z z'
  Srefl {i , d} refl = ∃i (↑ˢ i) (⋀i <ᵇ↑ˢ (⋀i <ᵇ↑ˢ refl))

  Ssymm : ∀{z z'} → S z z' → S z' z
  Ssymm {i , d} {i' , d'} (∃i j (⋀i p (⋀i p' e))) =
    ∃i j (⋀i p' (⋀i p (symm e)))

  Strans : ∀{z z' z''} → S z' z'' → S z z' → S z z''
  Strans {i , d} {i' , d'} {i'' , d''}
    (∃i k (⋀i q (⋀i q' e'))) (∃i j (⋀i p (⋀i p' e))) =
      ∃i l (⋀i r (⋀i r'' e''))
    where
    l : κ
    l = j ⊔ˢ k
    instance
      r : i <ᵇ l
      r = <ᵇ<ᵇ {{q = <ᵇ⊔ˢl}} {{p}}

      r' : i' <ᵇ l
      r' = <ᵇ<ᵇ {{q = <ᵇ⊔ˢr}} {{q}}

      r'' : i'' <ᵇ l
      r'' = <ᵇ<ᵇ {{q = <ᵇ⊔ˢr}} {{q'}}

    e'' : E D l i {{r}} d ≡ E D l i'' {{r''}} d''
    e'' =
      proof
        E D l i {{r}} d
      =[ ap (case d) (symm (E∙E D l j {{<ᵇ⊔ˢl}} i {{p}})) ]
        E D l j {{<ᵇ⊔ˢl}} (E D j i {{p}} d)
      =[ ap (E D l j {{<ᵇ⊔ˢl}}) e ]
        E D l j {{<ᵇ⊔ˢl}} (E D j i' {{p'}} d')
      =[ ap (case d') (E∙E D l j {{<ᵇ⊔ˢl}} i' {{p'}}) ]
        E D l i' {{r'}} d'
      =[ ap (case d') (symm (E∙E D l k {{<ᵇ⊔ˢr}} i' {{q}})) ]
        E D l k {{<ᵇ⊔ˢr}} (E D k i' {{q}} d')
      =[ ap (E D l k {{<ᵇ⊔ˢr}}) e' ]
        E D l k {{<ᵇ⊔ˢr}} (E D k i'' {{q'}} d'')
      =[ ap (case d'') (E∙E D l k {{<ᵇ⊔ˢr}} i'' {{q'}}) ]
        E D l i'' {{r''}} d''
      qed

----------------------------------------------------------------------
-- Isomorphisms in Set are bijections
----------------------------------------------------------------------
BijisIso :
  {A B : Set}
  (f : A → B)
  (_ : Bij f)
  → ---------
  Iso f
BijisIso {A} {B} f bij = ∃i finv (∧i lfinv rfinv)
  where
  instance
    ∃!x,fx=y :
      {y : B}
      → -----------------
      ∃! x ∶ A , f x ≡ y
    ∃!x,fx=y {y} =
      match bij \ where
        (∧i m e) → match (e y) \ where
          (∃i x refl) → ∃i x (∧i refl (λ _ e → symm (m e)))

  finv : B → A
  finv y = the x ∶ A , (f x ≡ y)

  lfinv : finv ∘ f ≡ id
  lfinv = funext \ x → the-uniq A (λ x' → f x' ≡ f x) x refl

  rfinv : f ∘ finv ≡ id
  rfinv = funext \ y → the-pf A (λ x → f x ≡ y)

invCong :
  {A : Set}
  {B C : A → Set}
  (f : (x : A) → B x → C x)
  {{_ : ∀ {x} → Iso (f x)}}
  (c : (x : A) → C x)
  {x x' : A}
  → ------------------------------------------
  x ≡ x' → ((f x)⁻¹) (c x) ≣ ((f x')⁻¹) (c x')
invCong _ _ refl = refl