module InitialAlgebra where

open import Axioms public
open import Prelude public

----------------------------------------------------------------------
-- Categories
----------------------------------------------------------------------
record Category (l m : Level)(𝓒 : Set l) : Set (l βŠ” lsuc m) where
  infixr 4 _⟢_
  infixr 5 _βˆ™_
  field
    _⟢_ : 𝓒 β†’ 𝓒 β†’ Set m
    ide : (X : 𝓒) β†’ (X ⟢ X)
    _βˆ™_ : {X Y Z : 𝓒} β†’ (Y ⟢ Z) β†’ (X ⟢ Y) β†’ (X ⟢ Z)
    ideβˆ™ :
      {X Y : 𝓒}
      {f : X ⟢ Y}
      β†’ -----------
      ide Y βˆ™ f ≑ f
    βˆ™ide :
      {X Y : 𝓒}
      {f : X ⟢ Y}
      β†’ -----------
      f βˆ™ ide X ≑ f
    βˆ™assoc :
      {X Y Z W : 𝓒}
      {f : X ⟢ Y}
      {g : Y ⟢ Z}
      {h : Z ⟢ W}
      β†’ ------------------------
      (h βˆ™ g) βˆ™ f ≑ h βˆ™ (g βˆ™ f)

open Category {{...}} public

{-# DISPLAY Category._⟢_ _ X Y = X ⟢ Y #-}
{-# DISPLAY Category._βˆ™_ _ g f = g βˆ™ f #-}

-- A useful lemma
βˆ™cong :
  {l m : Level}
  {𝓒 : Set l}
  {{_ : Category l m 𝓒}}
  {A A' B B' C C' : 𝓒}
  (g  : B  ⟢ C)
  (f  : A  ⟢ B)
  (g' : B' ⟢ C')
  (f' : A' ⟢ B')
  (_ : A ≑ A')
  (_ : B ≑ B')
  (_ : C ≑ C')

  (_ : f ≣ f')
  (_ : g ≣ g')
  β†’ -------------
  g βˆ™ f ≣ g' βˆ™ f'
βˆ™cong _ _ _ _ refl refl refl refl refl = refl

triangleq :
   {l m : Level}
   {𝓒 : Set l}
   {{_ : Category l m 𝓒}}
   {A A' B B' C C' : 𝓒}
   (f  : A  ⟢ B)
   (g  : B  ⟢ C)
   (h  : A  ⟢ C)
   (_ : A ≑ A')
   (_ : B ≑ B')
   (_ : C ≑ C')
   (f' : A' ⟢ B')
   (g' : B' ⟢ C')
   (h' : A' ⟢ C')
   (_ : f ≣ f')
   (_ : g ≣ g')
   (_ : h ≣ h')
   (_ : h' ≑  g' βˆ™ f')
   β†’ ---------------------
   h ≑ g βˆ™ f
triangleq _ _ _ refl refl refl _ _ _ refl refl refl e = e

-- Small categories
Cat : Set β†’ Set₁
Cat = Category β„“β‚€ β„“β‚€

-- Large, locally small categories
CAT : Set₁ β†’ Set₁
CAT = Category ℓ₁ β„“β‚€

----------------------------------------------------------------------
-- Functors
----------------------------------------------------------------------
record Functor
  {l l' m m' : Level}
  {𝓒 : Set l}
  {{_ : Category l m 𝓒}}
  {𝓒' : Set l'}
  {{_ : Category l' m' 𝓒'}}
  (F : 𝓒 β†’ 𝓒')
  : -----------------------
  Set (l βŠ” m βŠ” m')
  where
  field
     act : {X Y : 𝓒} β†’ (X ⟢ Y) β†’ (F X ⟢ F Y)
     actide :
       {X : 𝓒}
       β†’ ----------------------
       act (ide X) ≑ ide (F X)
     actβˆ™ :
       {X Y Z : 𝓒}
       {f : X ⟢ Y}
       {g : Y ⟢ Z}
       β†’ --------------------------
       act (g βˆ™ f) ≑ act g βˆ™ act f

open Functor {{...}} public

-- Notation for action of a functor on morphisms
infix 8 _β€²_
_β€²_ :
  {l l' m m' : Level}
  {𝓒 : Set l}
  {{_ : Category l m 𝓒}}
  {𝓒' : Set l'}
  {{_ : Category l' m' 𝓒'}}
  (F : 𝓒 β†’ 𝓒')
  {{_ : Functor F}}
  {X Y : 𝓒}
  (f : X ⟢ Y)
  β†’ ---------------
  F X ⟢ F Y
_ β€² f = act f

{-# DISPLAY Functor.act F f = F β€² f #-}

-- Identity functor
FunctorId :
  {l m : Level}
  {𝓒 : Set l}
  {{_ : Category l m 𝓒}}
  β†’ --------------------
  Functor Ξ» (X : 𝓒) β†’ X
act    {{FunctorId}} = id
actide {{FunctorId}} = refl
actβˆ™   {{FunctorId}} = refl

-- Composition of functors
FunctorComp :
  {l l' l'' m m' m'' : Level}
  {𝓒 : Set l}
  {{_ : Category l m 𝓒}}
  {𝓒' : Set l'}
  {{_ : Category l' m' 𝓒'}}
  {𝓒'' : Set l''}
  {{_ : Category l'' m'' 𝓒''}}
  (F : 𝓒 β†’ 𝓒')
  {{_ : Functor F}}
  (F' : 𝓒' β†’ 𝓒'')
  {{_ : Functor F'}}
  β†’ --------------------------
  Functor (F' ∘ F)
act    {{FunctorComp F F'}} f            = F' β€² (F β€² f)
actide {{FunctorComp F F'}} {X}          =
  proof
    F' β€² (F β€² (ide X))
  =[ ap (F' β€²_) (actide {F = F}) ]
    F' β€² (ide (F X))
  =[ actide {F = F'} ]
    ide (F'(F X))
  qed
actβˆ™   {{FunctorComp F F'}} {f = f} {g}  =
  proof
    F' β€² (F β€² (g βˆ™ f))
  =[ ap (F' β€²_) (actβˆ™ {F = F}) ]
    F' β€² (F β€² g βˆ™ F β€² f)
  =[ actβˆ™ {F = F'} ]
    (F' β€² (F β€² g)) βˆ™ (F' β€² (F β€² f))
  qed

----------------------------------------------------------------------
-- Isomorphisms
----------------------------------------------------------------------
Iso :
  {l m : Level}
  {𝓒 : Set l}
  {{_ : Category l m 𝓒}}
  {X Y : 𝓒}
  β†’ --------------------
  (X ⟢ Y) β†’ Prop m
Iso {X = X} {Y} f = βˆƒ g ∢ (Y ⟢ X), iso g
  module _ where
  iso : (Y ⟢ X) β†’ Prop _
  iso g = g βˆ™ f ≑ ide X ∧ f βˆ™ g ≑ ide Y

module _
  {l m : Level}
  {𝓒 : Set l}
  {{_ : Category l m 𝓒}}
  {X Y : 𝓒}
  (f : X ⟢ Y)
  {{u : Iso f}}
  where
  private
    v : βˆƒ! (Y ⟢ X) (iso f)
    v = match u \ where
      (βˆƒi g invg@(∧i _ r)) β†’ βˆƒi g (∧i invg Ξ»{g' (∧i l' _) β†’
        proof
          g
        =[ symm ideβˆ™ ]
          ide X βˆ™ g
        =[ ap (_βˆ™ g) (symm l') ]
          (g' βˆ™ f) βˆ™ g
        =[ βˆ™assoc ]
          g' βˆ™ (f βˆ™ g)
        =[ ap (g' βˆ™_) r ]
          g' βˆ™ ide Y
        =[ βˆ™ide ]
          g'
        qed})

  _⁻¹ : Y ⟢ X
  _⁻¹ = the (Y ⟢ X) (iso f) {{v}}

  linv : _⁻¹ βˆ™ f ≑ ide X
  linv = ∧e₁ (the-pf (Y ⟢ X) (iso f) {{v}})

  rinv : f βˆ™ _⁻¹ ≑ ide Y
  rinv = ∧eβ‚‚ (the-pf (Y ⟢ X) (iso f) {{v}})

---------------------------------------------------------------------
-- Algebras for endofunctors
----------------------------------------------------------------------
record Alg
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  (F : 𝓒 β†’ 𝓒)
  {{_ : Functor F}}
  (A : 𝓒)
  : ---------------
  Set₁
  where
  constructor mkAlg
  field
    fold : F A ⟢ A

open Alg{{...}} public

-- The property of being an algebra morphism
AlgHom :
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  (F : 𝓒 β†’ 𝓒)
  {{_ : Functor F}}
  {A A' : 𝓒}
  {{_ : Alg F A}}
  {{_ : Alg F A'}}
  (h : A ⟢ A')
  β†’ ---------------
  Prop
AlgHom F h = h βˆ™ fold ≑ fold βˆ™ F β€² h

AlgHomide :
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {F : 𝓒 β†’ 𝓒}
  {{_ : Functor F}}
  {A : 𝓒}
  {{_ : Alg F A}}
  β†’ ---------------
  AlgHom F (ide A)
AlgHomide {F = F} {A} =
  proof
    ide A βˆ™ fold
  =[ ideβˆ™ ]
    fold
  =[ symm βˆ™ide ]
    fold βˆ™ ide (F A)
  =[ ap (fold βˆ™_) (symm actide) ]
    fold βˆ™ F β€² (ide A)
  qed

AlgHomβˆ™ :
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  {F : 𝓒 β†’ 𝓒}
  {{_ : Functor F}}
  {A B C : 𝓒}
  {{_ : Alg F A}}
  {{_ : Alg F B}}
  {{_ : Alg F C}}
  {f : A ⟢ B}
  (_ : AlgHom F f)
  {g : B ⟢ C}
  (_ : AlgHom F g)
  β†’ ----------------
  AlgHom F (g βˆ™ f)
AlgHomβˆ™ {F = F} {A} {B} {f = f} fa {g} ga =
  proof
    (g βˆ™ f) βˆ™ fold {A = A}
  =[ βˆ™assoc ]
    g βˆ™ (f βˆ™ fold {A = A})
  =[ ap (g βˆ™_) fa ]
    g βˆ™ (fold {A = B} βˆ™ F β€² f)
  =[ symm βˆ™assoc ]
    (g βˆ™ fold {A = B}) βˆ™ F β€² f
  =[ ap (_βˆ™ F β€² f) ga ]
    (fold βˆ™ F β€² g) βˆ™ F β€² f
  =[ βˆ™assoc ]
    fold βˆ™ (F β€² g βˆ™ F β€² f)
  =[ ap (fold βˆ™_) (symm actβˆ™) ]
    fold βˆ™ F β€² (g βˆ™ f)
  qed

----------------------------------------------------------------------
-- Definition of intial algebra on an endofunctor
----------------------------------------------------------------------
record InitialAlg
  {𝓒 : Set₁}
  {{_ : CAT 𝓒}}
  (F : 𝓒 β†’ 𝓒)
  {{_ : Functor F}}
  : ---------------
  Set₁
  where
  field
    obj     : 𝓒
    {{alg}} : Alg F obj
    fun     : (A : 𝓒){{_ : Alg F A}} β†’ (obj ⟢ A)
    hom     : (A : 𝓒){{_ : Alg F A}} β†’ AlgHom F (fun A)
    unq     :
      (A : 𝓒)
      {{_ : Alg F A}}
      {f : obj ⟢ A}
      (_ : AlgHom F f)
      β†’ --------------
      fun A ≑ f