module InitialAlgebra where
open import Axioms public
open import Prelude public
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 #-}
β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
Cat : Set β Setβ
Cat = Category ββ ββ
CAT : Setβ β Setβ
CAT = Category ββ ββ
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
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 #-}
FunctorId :
{l m : Level}
{π : Set l}
{{_ : Category l m π}}
β
Functor Ξ» (X : π) β X
act {{FunctorId}} = id
actide {{FunctorId}} = refl
actβ {{FunctorId}} = refl
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
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}})
record Alg
{π : Setβ}
{{_ : CAT π}}
(F : π β π)
{{_ : Functor F}}
(A : π)
:
Setβ
where
constructor mkAlg
field
fold : F A βΆ A
open Alg{{...}} public
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
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