Library Beroal.CategoryTheory

Basics of category theory. Category, monad, functor, natural transformation, adjunction, monad.

Uses axioms:
  • extensional equality of functions;
  • proof-irrelevance.
Does not use embedding of Haskell classes into Coq; Coq modules.

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

Category


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
}.

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.

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.

Functor


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.

Natural transformation


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).

Composition of NT-s and functors, facts



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.

auxilary
Definition frl := fun (cat0 cat1:sigT category) (fr:functor cat0 cat1)
        => fr # fr_id _.

Adjunction


Section adjunction.

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].

Monad


Section md.
Variable (cat:sigT category).

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.

Algebra over a monad


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.