Library Beroal.CategoryTheory
Basics of category theory. Category, monad, functor, natural transformation, adjunction, monad.
Uses axioms:
Notations. Every structure (e.g. functor) is divided into two parts: x_set and x_prop. x_set contains "data" and x_prop contains axioms/laws which data satisfies. We need this splitting when comparing structures using sig_eq.
Uses axioms:
- extensional equality of functions;
- proof-irrelevance.
Notations. Every structure (e.g. functor) is divided into two parts: x_set and x_prop. x_set contains "data" and x_prop contains axioms/laws which data satisfies. We need this splitting when comparing structures using sig_eq.
- ob = object
- mor = morphism
- id = identity morphism
- comp = composition of morphisms
- fr = functor
- nt = natural transformation
- md = monad
- adj = adjunction
Require Import Coq.Logic.ProofIrrelevance.
Require Beroal.Init.
Require Beroal.FunExtEq.
Definition sig_eq := Beroal.Init.sig_eq proof_irrelevance.
Definition fun_ext_eq := Beroal.FunExtEq.ext_eq_dep.
category does not containt a type of objects. Instead a type of objects is a parameter. Then we define functor category as category, we do not need to duplicate category Record.
Record category (ob : Type) : Type :=
{ hom : ob -> ob -> Type
; id : forall ob1:ob, hom ob1 ob1
; comp : forall ob1 ob2 ob3:ob, hom ob2 ob3
-> hom ob1 ob2 -> hom ob1 ob3
; id_left : forall (ob1 ob2:ob) (m:hom ob1 ob2),
m = comp (id _) m
; id_right : forall (ob1 ob2:ob) (m:hom ob1 ob2),
m = comp m (id _)
; comp_assoc : forall (ob1 ob2 ob3 ob4:ob)
(m34: hom ob3 ob4) (m23: hom ob2 ob3) (m12: hom ob1 ob2),
comp m34 (comp m23 m12)
= comp (comp m34 m23) m12
}.
{ hom : ob -> ob -> Type
; id : forall ob1:ob, hom ob1 ob1
; comp : forall ob1 ob2 ob3:ob, hom ob2 ob3
-> hom ob1 ob2 -> hom ob1 ob3
; id_left : forall (ob1 ob2:ob) (m:hom ob1 ob2),
m = comp (id _) m
; id_right : forall (ob1 ob2:ob) (m:hom ob1 ob2),
m = comp m (id _)
; comp_assoc : forall (ob1 ob2 ob3 ob4:ob)
(m34: hom ob3 ob4) (m23: hom ob2 ob3) (m12: hom ob1 ob2),
comp m34 (comp m23 m12)
= comp (comp m34 m23) m12
}.
We need this Record to allow Coq automatically infer domain and codomain of a morphism. We can't use hom.
Record homi (cat : sigT category) (dom cod : projT1 cat) : Type
:= {un_homi : hom (projT2 cat) dom cod}.
Section homi.
Variable (cat:sigT category).
Definition idi := fun (ob0:projT1 cat)
=> Build_homi _ _ _ (id _ ob0).
Definition compi := fun (ob0 ob1 ob2:projT1 cat)
(m12 : homi cat ob1 ob2) (m01 : homi cat ob0 ob1)
=> Build_homi _ _ _ (comp _ _ _ _ (un_homi m12) (un_homi m01)).
End homi.
:= {un_homi : hom (projT2 cat) dom cod}.
Section homi.
Variable (cat:sigT category).
Definition idi := fun (ob0:projT1 cat)
=> Build_homi _ _ _ (id _ ob0).
Definition compi := fun (ob0 ob1 ob2:projT1 cat)
(m12 : homi cat ob1 ob2) (m01 : homi cat ob0 ob1)
=> Build_homi _ _ _ (comp _ _ _ _ (un_homi m12) (un_homi m01)).
End homi.
composition of morphisms
Notation "a * b" := (compi a b) (at level 40, left associativity).
Section homi_fact.
Variable (cat:sigT category).
Definition id_lefti : forall (ob0 ob1:projT1 cat) (m:homi cat ob0 ob1),
m = idi _ _ * m.
Definition id_righti : forall (ob0 ob1:projT1 cat) (m:homi cat ob0 ob1),
m = m * idi _ _.
Definition comp_associ : forall (ob0 ob1 ob2 ob3:projT1 cat)
(m23: homi cat ob2 ob3) (m12: homi cat ob1 ob2)
(m01: homi cat ob0 ob1),
m23 * (m12 * m01) = (m23 * m12) * m01.
End homi_fact.
Section homi_fact.
Variable (cat:sigT category).
Definition id_lefti : forall (ob0 ob1:projT1 cat) (m:homi cat ob0 ob1),
m = idi _ _ * m.
Definition id_righti : forall (ob0 ob1:projT1 cat) (m:homi cat ob0 ob1),
m = m * idi _ _.
Definition comp_associ : forall (ob0 ob1 ob2 ob3:projT1 cat)
(m23: homi cat ob2 ob3) (m12: homi cat ob1 ob2)
(m01: homi cat ob0 ob1),
m23 * (m12 * m01) = (m23 * m12) * m01.
End homi_fact.
Section functor.
Variable (cat_dom cat_cod:sigT category).
Let ob_dom := projT1 cat_dom.
Let ob_cod := projT1 cat_cod.
Record functor_set:Type
:= { frs_ob : ob_dom -> ob_cod
; frs_mor : forall dom cod : ob_dom,
homi cat_dom dom cod
-> homi cat_cod (frs_ob dom) (frs_ob cod)
}.
Record functor_prop(fr0:functor_set):Prop
:= { frs_pres_id : forall ob0:ob_dom, idi _ _ = frs_mor fr0 (idi _ ob0)
; frs_pres_comp : forall (ob0 ob1 ob2:ob_dom)
(m12:homi cat_dom ob1 ob2) (m01:homi cat_dom ob0 ob1),
frs_mor fr0 m12 * frs_mor fr0 m01 = frs_mor fr0 (m12 * m01)
}.
Definition functor := sig functor_prop.
Section functor_proj.
Variable fr0:functor.
Definition fr_ob := frs_ob (proj1_sig fr0).
Definition fr_mor := frs_mor (proj1_sig fr0).
End functor_proj.
Section nt.
Variable fr0 fr1:functor.
Definition nt_set := forall obd:ob_dom,
homi cat_cod (fr_ob fr0 obd) (fr_ob fr1 obd).
Definition nt_prop := fun nt0:nt_set
=> forall (obd obc:ob_dom) (m:homi cat_dom obd obc),
fr_mor fr1 m * nt0 obd = nt0 obc * fr_mor fr0 m.
Definition nt := sig nt_prop.
Section nt_proj.
Variable nt0:nt.
Definition ntf := proj1_sig nt0.
Definition nt_mor_comm := proj2_sig nt0.
End nt_proj.
Definition nt_eq_set := fun nt0 nt1 => ntf nt0 = ntf nt1.
End nt.
Section nt_id.
Variable fr0:functor.
Definition nt_id_set := (fun obd => idi cat_cod (fr_ob fr0 obd)
) : nt_set fr0 fr0.
Definition nt_id_prop : nt_prop nt_id_set.
Definition nt_id := (exist _ nt_id_set nt_id_prop
) : nt fr0 fr0.
End nt_id.
Section nt_comp.
Variable (fr0 fr1 fr2:functor) .
Definition nt_comp_set := fun (nt12:nt_set fr1 fr2) (nt01:nt_set fr0 fr1)
=> (fun obd => nt12 obd * nt01 obd
) : nt_set fr0 fr2.
Variable (nt12:nt fr1 fr2) (nt01:nt fr0 fr1).
Definition nt_comp_prop : nt_prop (nt_comp_set (ntf nt12) (ntf nt01)).
Definition nt_comp := (exist _
(nt_comp_set (ntf nt12) (ntf nt01)) nt_comp_prop
) : nt fr0 fr2.
End nt_comp.
functor category
Definition fr_cat : category (functor).
End functor.
Notation "a =@ b" := (nt_eq_set a b) (at level 70, no associativity).
Notation "a @ b" := (nt_comp a b) (at level 40, left associativity).
Notation "a @$ b" := (nt_comp_set a b) (at level 40, left associativity).
Section fr_id.
Variable cat0:sigT category.
Definition fr_id_set := (Build_functor_set (fun a=>a) (fun _ _ a=>a)
) : functor_set cat0 cat0.
Definition fr_id_prop : functor_prop fr_id_set.
Definition fr_id := (exist _ fr_id_set fr_id_prop
) : functor cat0 cat0.
End fr_id.
Section fr_comp.
Variable (cat0 cat1 cat2:sigT category).
Definition fr_comp_set := fun (fr12 : functor_set cat1 cat2)
(fr01 : functor_set cat0 cat1)
=> (Build_functor_set
(fun a => frs_ob fr12 (frs_ob fr01 a))
(fun _ _ a => frs_mor fr12 (frs_mor fr01 a))
) : functor_set cat0 cat2.
Variable (fr12 : functor cat1 cat2) (fr01 : functor cat0 cat1).
Definition fr_comp_prop
: functor_prop (fr_comp_set (proj1_sig fr12) (proj1_sig fr01)).
Definition fr_comp := (exist _
(fr_comp_set (proj1_sig fr12) (proj1_sig fr01))
fr_comp_prop
) : functor cat0 cat2.
End fr_comp.
Notation "a # b" := (fr_comp a b) (at level 40, left associativity).
Notation "a #$ b" := (fr_comp_set a b) (at level 40, left associativity).
Section comp_nt_fr_ob.
Variable (cat0 cat1 cat2:sigT category) (fr0 fr1:functor cat1 cat2).
Definition comp_nt_fr_ob_set := fun (nt0:nt_set fr0 fr1)
(fr2:functor cat0 cat1)
=> (fun oba => nt0 (fr_ob fr2 oba)
) : nt_set (fr0 # fr2) (fr1 # fr2).
Variable (nt0:nt fr0 fr1) (fr2:functor cat0 cat1).
Definition comp_nt_fr_ob_prop
: nt_prop (comp_nt_fr_ob_set (ntf nt0) fr2).
Definition comp_nt_fr_ob := (exist _
(comp_nt_fr_ob_set (ntf nt0) fr2)
comp_nt_fr_ob_prop
) : nt (fr0 # fr2) (fr1 # fr2).
End comp_nt_fr_ob.
Notation "a '> b" := (comp_nt_fr_ob a b)
(at level 25, left associativity).
Notation "a >$ b" := (comp_nt_fr_ob_set a b)
(at level 25, left associativity).
Section comp_nt_fr_mor.
Variable (cat0 cat1 cat2:sigT category)
(fr0 fr1:functor cat0 cat1).
Definition comp_nt_fr_mor_set := fun (fr2:functor cat1 cat2)
(nt0:nt_set fr0 fr1)
=> (fun oba => fr_mor fr2 (nt0 oba)
) : nt_set (fr2 # fr0) (fr2 # fr1).
Variable (fr2:functor cat1 cat2) (nt0:nt fr0 fr1).
Definition comp_nt_fr_mor_prop
: nt_prop (comp_nt_fr_mor_set fr2 (ntf nt0)).
Definition comp_nt_fr_mor := (exist _
(comp_nt_fr_mor_set fr2 (ntf nt0)) comp_nt_fr_mor_prop
) : nt (fr2 # fr0) (fr2 # fr1).
End comp_nt_fr_mor.
Notation "a <' b" := (comp_nt_fr_mor a b)
(at level 20, right associativity).
Notation "a <$ b" := (comp_nt_fr_mor_set a b)
(at level 20, right associativity).
End functor.
Notation "a =@ b" := (nt_eq_set a b) (at level 70, no associativity).
Notation "a @ b" := (nt_comp a b) (at level 40, left associativity).
Notation "a @$ b" := (nt_comp_set a b) (at level 40, left associativity).
Section fr_id.
Variable cat0:sigT category.
Definition fr_id_set := (Build_functor_set (fun a=>a) (fun _ _ a=>a)
) : functor_set cat0 cat0.
Definition fr_id_prop : functor_prop fr_id_set.
Definition fr_id := (exist _ fr_id_set fr_id_prop
) : functor cat0 cat0.
End fr_id.
Section fr_comp.
Variable (cat0 cat1 cat2:sigT category).
Definition fr_comp_set := fun (fr12 : functor_set cat1 cat2)
(fr01 : functor_set cat0 cat1)
=> (Build_functor_set
(fun a => frs_ob fr12 (frs_ob fr01 a))
(fun _ _ a => frs_mor fr12 (frs_mor fr01 a))
) : functor_set cat0 cat2.
Variable (fr12 : functor cat1 cat2) (fr01 : functor cat0 cat1).
Definition fr_comp_prop
: functor_prop (fr_comp_set (proj1_sig fr12) (proj1_sig fr01)).
Definition fr_comp := (exist _
(fr_comp_set (proj1_sig fr12) (proj1_sig fr01))
fr_comp_prop
) : functor cat0 cat2.
End fr_comp.
Notation "a # b" := (fr_comp a b) (at level 40, left associativity).
Notation "a #$ b" := (fr_comp_set a b) (at level 40, left associativity).
Section comp_nt_fr_ob.
Variable (cat0 cat1 cat2:sigT category) (fr0 fr1:functor cat1 cat2).
Definition comp_nt_fr_ob_set := fun (nt0:nt_set fr0 fr1)
(fr2:functor cat0 cat1)
=> (fun oba => nt0 (fr_ob fr2 oba)
) : nt_set (fr0 # fr2) (fr1 # fr2).
Variable (nt0:nt fr0 fr1) (fr2:functor cat0 cat1).
Definition comp_nt_fr_ob_prop
: nt_prop (comp_nt_fr_ob_set (ntf nt0) fr2).
Definition comp_nt_fr_ob := (exist _
(comp_nt_fr_ob_set (ntf nt0) fr2)
comp_nt_fr_ob_prop
) : nt (fr0 # fr2) (fr1 # fr2).
End comp_nt_fr_ob.
Notation "a '> b" := (comp_nt_fr_ob a b)
(at level 25, left associativity).
Notation "a >$ b" := (comp_nt_fr_ob_set a b)
(at level 25, left associativity).
Section comp_nt_fr_mor.
Variable (cat0 cat1 cat2:sigT category)
(fr0 fr1:functor cat0 cat1).
Definition comp_nt_fr_mor_set := fun (fr2:functor cat1 cat2)
(nt0:nt_set fr0 fr1)
=> (fun oba => fr_mor fr2 (nt0 oba)
) : nt_set (fr2 # fr0) (fr2 # fr1).
Variable (fr2:functor cat1 cat2) (nt0:nt fr0 fr1).
Definition comp_nt_fr_mor_prop
: nt_prop (comp_nt_fr_mor_set fr2 (ntf nt0)).
Definition comp_nt_fr_mor := (exist _
(comp_nt_fr_mor_set fr2 (ntf nt0)) comp_nt_fr_mor_prop
) : nt (fr2 # fr0) (fr2 # fr1).
End comp_nt_fr_mor.
Notation "a <' b" := (comp_nt_fr_mor a b)
(at level 20, right associativity).
Notation "a <$ b" := (comp_nt_fr_mor_set a b)
(at level 20, right associativity).
Definition comp_nt_fr_mor_distrib_set
: forall (cat0 cat1 cat2:sigT category)
(fr12:functor cat1 cat2)
(fra frb frc:functor cat0 cat1)
(ntbc:nt_set frb frc) (ntab:nt_set fra frb),
(fr12 <$ ntbc) @$ (fr12 <$ ntab) = fr12 <$ (ntbc @$ ntab).
Definition comp_nt_fr_mor_set_id : forall
(cat0 cat1 cat2:sigT category)
(fr12:functor cat1 cat2)
(fr01:functor cat0 cat1),
nt_id_set (fr12 # fr01) = fr12 <$ nt_id_set fr01.
Definition comp_nt_fr_mor_id : forall
(cat0 cat1 cat2:sigT category)
(fr12:functor cat1 cat2)
(fr01:functor cat0 cat1),
nt_id (fr12 # fr01) = fr12 <' nt_id fr01.
NT-s commute in the definition of Godement multiplication = horizontal composition
Definition nt_comm : forall (cat0 cat1 cat2:sigT category)
(A0 A1 : functor cat0 cat1)
(A : nt A0 A1)
(B0 B1 : functor cat1 cat2)
(B : nt B0 B1),
B1 <' A @ B '> A0 =@ B '> A1 @ B0 <' A.
(A0 A1 : functor cat0 cat1)
(A : nt A0 A1)
(B0 B1 : functor cat1 cat2)
(B : nt B0 B1),
B1 <' A @ B '> A0 =@ B '> A1 @ B0 <' A.
auxilary
Example. cats is a category of sets, cata is a category of algebraic systems with a fixed signature. F is a free functor, U is an underlying functor. ret = η, fold = ε. Example. cata is a category of monoids. F = list. On monoid ⟨nat,plus,0⟩ "fold" is usual folding of a list nat with plus and 0.
Variable cats cata : sigT category.
Record adjunction_set:Type
:= { adjsF : functor cats cata; adjsU : functor cata cats
; adjs_ret : nt (fr_id _) (adjsU # adjsF)
; adjs_fold : nt (adjsF # adjsU) (fr_id _)
}.
Record adjunction_prop (s:adjunction_set) : Prop
:= { adjs_nt_eq_u : nt_id (frl (adjsU s))
=@ (adjsU s) <' (adjs_fold s) @ (adjs_ret s) '> (adjsU s)
; adjs_nt_eq_f : nt_id (frl (adjsF s))
=@ (adjs_fold s) '> (adjsF s) @ (adjsF s) <' (adjs_ret s)
}.
Definition adjunction := sig adjunction_prop.
Section adjunction_proj.
Variable a:adjunction.
Definition adjF := adjsF (proj1_sig a).
Definition adjU := adjsU (proj1_sig a).
Definition adj_ret := adjs_ret (proj1_sig a).
Definition adj_fold := adjs_fold (proj1_sig a).
End adjunction_proj.
End adjunction.
Implicit Arguments Build_adjunction_set [cats cata].
ret = η, join = μ
Record md_set:Type
:= { mds_fr : functor cat cat
; mds_ret : nt (fr_id _) (frl mds_fr)
; mds_join : nt (mds_fr # mds_fr) (frl mds_fr)
}.
Record md_prop (s:md_set) : Prop
:= { mds_id_left : nt_id (frl (mds_fr s))
=@ mds_join s @ (mds_ret s '> mds_fr s)
; mds_id_right : nt_id (frl (mds_fr s))
=@ mds_join s @ (mds_fr s <' mds_ret s)
; mds_assoc : mds_join s @ (mds_join s '> mds_fr s)
=@ mds_join s @ (mds_fr s <' mds_join s)
}.
Definition md := sig md_prop.
Section md_proj.
Variable m:md.
Definition md_fr := mds_fr (proj1_sig m).
Definition md_ret := mds_ret (proj1_sig m).
Definition md_join := mds_join (proj1_sig m).
End md_proj.
:= { mds_fr : functor cat cat
; mds_ret : nt (fr_id _) (frl mds_fr)
; mds_join : nt (mds_fr # mds_fr) (frl mds_fr)
}.
Record md_prop (s:md_set) : Prop
:= { mds_id_left : nt_id (frl (mds_fr s))
=@ mds_join s @ (mds_ret s '> mds_fr s)
; mds_id_right : nt_id (frl (mds_fr s))
=@ mds_join s @ (mds_fr s <' mds_ret s)
; mds_assoc : mds_join s @ (mds_join s '> mds_fr s)
=@ mds_join s @ (mds_fr s <' mds_join s)
}.
Definition md := sig md_prop.
Section md_proj.
Variable m:md.
Definition md_fr := mds_fr (proj1_sig m).
Definition md_ret := mds_ret (proj1_sig m).
Definition md_join := mds_join (proj1_sig m).
End md_proj.
Section alg_md.
Variable m:md.
Record alg_md_set:Type
:= { ams_ob : projT1 cat
; ams_fold : homi cat (fr_ob (md_fr m) ams_ob) ams_ob
}.
Record alg_md_prop (s:alg_md_set) : Prop
:= { ams_unit : idi _ _ = ams_fold s * (ntf (md_ret m) (ams_ob s))
; ams_assoc : ams_fold s * (ntf (md_join m) (ams_ob s))
= ams_fold s * (fr_mor (md_fr m) (ams_fold s))
}.
Definition alg_md := sig alg_md_prop.
End alg_md.
End md.
Implicit Arguments Build_md_set [cat].
Implicit Arguments Build_alg_md_set [cat].
Implicit Arguments Build_alg_md_prop [cat].
⟨T C,μ C⟩ is an algebra over a monad
Section alg_join.
Variable (cat:sigT category) (m:md cat) (C:projT1 cat).
Definition alg_join_set := Build_alg_md_set m
(fr_ob (md_fr m) C) (ntf (md_join m) C).
Definition alg_join_prop : alg_md_prop alg_join_set.
Definition alg_join := (exist _ alg_join_set alg_join_prop
) : alg_md m.
End alg_join.
canonical conversion of an adjunction into a monad
Section adj2md.
Variable (cats cata:sigT category) (a:adjunction cats cata).
Definition adj2md_set := (Build_md_set
(adjU a # adjF a) (adj_ret a)
(adjU a <' adj_fold a '> adjF a)
) : md_set cats.
Definition adj2md_prop : md_prop adj2md_set.
Definition adj2md := (exist _ adj2md_set adj2md_prop) : md cats.
⟨U C,U ε C⟩ is an algebra over a monad
Section alg_fold.
Variable C:projT1 cata.
Definition alg_fold_set := Build_alg_md_set adj2md
(fr_ob (adjU a) C) (ntf (adjU a <' adj_fold a) C).
Definition alg_fold_prop : alg_md_prop alg_fold_set.
Eval unfold alg_md in alg_md adj2md.
Definition alg_fold := (exist _ alg_fold_set alg_fold_prop
) : alg_md adj2md.
End alg_fold.
End adj2md.