Definition: small-category
SmallCategory ==
  {cat:ob:Type
   × arrow:ob ⟶ ob ⟶ Type
   × x:ob ⟶ (arrow x x)
   × (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z))| 
   let ob,arrow,id,comp = cat 
   in (∀x,y:ob. ∀f:arrow x y.  (((comp x x y (id x) f) = f ∈ (arrow x y)) ∧ ((comp x y y f (id y)) = f ∈ (arrow x y))))
      ∧ (∀x,y,z,w:ob. ∀f:arrow x y. ∀g:arrow y z. ∀h:arrow z w.
           ((comp x z w (comp x y z f g) h) = (comp x y w f (comp y z w g h)) ∈ (arrow x w)))  } 
Lemma: small-category_wf
SmallCategory ∈ 𝕌'
Lemma: small-category-subtype
SmallCategory ⊆r SmallCategory'
Lemma: small-category-subtype'
SmallCategory ⊆r small-category{i'':l}
Definition: cat-ob
cat-ob(C) ==  fst(C)
Lemma: cat-ob_wf
∀[C:SmallCategory]. (cat-ob(C) ∈ Type)
Lemma: cat_ob_pair_lemma
∀y,x:Top.  (cat-ob(<x, y>) ~ x)
Definition: cat-arrow
cat-arrow(C) ==  fst(snd(C))
Lemma: cat-arrow_wf
∀[C:SmallCategory]. (cat-arrow(C) ∈ x:cat-ob(C) ⟶ y:cat-ob(C) ⟶ Type)
Lemma: cat_arrow_triple_lemma
∀y,x,ob:Top.  (cat-arrow(<ob, x, y>) ~ x)
Definition: cat-id
cat-id(C) ==  fst(snd(snd(C)))
Lemma: cat-id_wf
∀[C:SmallCategory]. (cat-id(C) ∈ x:cat-ob(C) ⟶ (cat-arrow(C) x x))
Lemma: cat_id_tuple_lemma
∀y,x,arrow,ob:Top.  (cat-id(<ob, arrow, x, y>) ~ x)
Definition: cat-comp
cat-comp(C) ==  snd(snd(snd(C)))
Lemma: cat-comp_wf
∀[C:SmallCategory]
  (cat-comp(C) ∈ x:cat-ob(C)
   ⟶ y:cat-ob(C)
   ⟶ z:cat-ob(C)
   ⟶ (cat-arrow(C) x y)
   ⟶ (cat-arrow(C) y z)
   ⟶ (cat-arrow(C) x z))
Lemma: cat_comp_tuple_lemma
∀y,x,arrow,ob:Top.  (cat-comp(<ob, arrow, x, y>) ~ y)
Definition: cat_comp
g o f ==  cat-comp(C) x y z f g
Lemma: cat_comp_wf
∀[C:SmallCategory]. ∀[x,y,z:cat-ob(C)]. ∀[f:cat-arrow(C) x y]. ∀[g:cat-arrow(C) y z].  (g o f ∈ cat-arrow(C) x z)
Definition: mk-cat
Cat(ob = ob;
    arrow(x,y) = arrow[x; y];
    id(a) = id[a];
    comp(u,v,w,f,g) = comp[u; v; w; f; g]) ==
  <ob, λx,y. arrow[x; y], λa.id[a], λu,v,w,f,g. comp[u; v; w; f; g]>
Lemma: mk-cat_wf
∀[ob:Type]. ∀[arrow:ob ⟶ ob ⟶ Type]. ∀[id:x:ob ⟶ arrow[x;x]]. ∀[comp:x:ob
                                                                        ⟶ y:ob
                                                                        ⟶ z:ob
                                                                        ⟶ arrow[x;y]
                                                                        ⟶ arrow[y;z]
                                                                        ⟶ arrow[x;z]].
  (Cat(ob = ob;
       arrow(x,y) = arrow[x;y];
       id(a) = id[a];
       comp(u,v,w,f,g) = comp[u;v;w;f;g]) ∈ SmallCategory) supposing 
     ((∀x,y,z,w:ob. ∀f:arrow[x;y]. ∀g:arrow[y;z]. ∀h:arrow[z;w].
         (comp[x;z;w;comp[x;y;z;f;g];h] = comp[x;y;w;f;comp[y;z;w;g;h]] ∈ arrow[x;w])) and 
     (∀x,y:ob. ∀f:arrow[x;y].  ((comp[x;x;y;id[x];f] = f ∈ arrow[x;y]) ∧ (comp[x;y;y;f;id[y]] = f ∈ arrow[x;y]))))
Definition: tree-cat
tree-cat(X) ==  Cat(ob = X;arrow(x,y) = Unit;id(a) = ⋅;comp(u,v,w,f,g) = ⋅)
Lemma: tree-cat_wf
∀[X:Type]. (tree-cat(X) ∈ SmallCategory)
Definition: discrete-cat
discrete-cat(X) ==  Cat(ob = X;arrow(x,y) = x = y ∈ X;id(a) = ⋅;comp(u,v,w,f,g) = ⋅)
Lemma: discrete-cat_wf
∀[X:Type]. (discrete-cat(X) ∈ SmallCategory)
Definition: unit-cat
1 ==  discrete-cat(Unit)
Lemma: unit-cat_wf
1 ∈ SmallCategory
Definition: cat-inverse
fg=1 ==  (cat-comp(C) x y x f g) = (cat-id(C) x) ∈ (cat-arrow(C) x x)
Lemma: cat-inverse_wf
∀[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x y]. ∀[g:cat-arrow(C) y x].  (fg=1 ∈ ℙ)
Definition: cat-co-retraction
co-retraction(f) ==  ∃g:cat-arrow(C) y x. fg=1
Lemma: cat-co-retraction_wf
∀[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x y].  (co-retraction(f) ∈ ℙ)
Definition: cat-retraction
retraction(g) ==  ∃f:cat-arrow(C) x y. fg=1
Lemma: cat-retraction_wf
∀[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[g:cat-arrow(C) y x].  (retraction(g) ∈ ℙ)
Lemma: cat-comp-assoc
∀[C:SmallCategory]
  ∀x,y,z,w:cat-ob(C). ∀f:cat-arrow(C) x y. ∀g:cat-arrow(C) y z. ∀h:cat-arrow(C) z w.
    ((cat-comp(C) x z w (cat-comp(C) x y z f g) h) = (cat-comp(C) x y w f (cat-comp(C) y z w g h)) ∈ (cat-arrow(C) x w))
Lemma: cat_comp_assoc
∀[C:SmallCategory]
  ∀x,y,z,w:cat-ob(C). ∀f:cat-arrow(C) x y. ∀g:cat-arrow(C) y z. ∀h:cat-arrow(C) z w.
    (h o g o f = h o g o f ∈ (cat-arrow(C) x w))
Lemma: cat-comp-ident
∀[C:SmallCategory]
  ∀x,y:cat-ob(C). ∀f:cat-arrow(C) x y.
    (((cat-comp(C) x x y (cat-id(C) x) f) = f ∈ (cat-arrow(C) x y))
    ∧ ((cat-comp(C) x y y f (cat-id(C) y)) = f ∈ (cat-arrow(C) x y)))
Lemma: cat-comp-ident1
∀[C:SmallCategory]. ∀x,y:cat-ob(C). ∀f:cat-arrow(C) x y.  ((cat-comp(C) x x y (cat-id(C) x) f) = f ∈ (cat-arrow(C) x y))
Lemma: cat-comp-ident2
∀[C:SmallCategory]. ∀x,y:cat-ob(C). ∀f:cat-arrow(C) x y.  ((cat-comp(C) x y y f (cat-id(C) y)) = f ∈ (cat-arrow(C) x y))
Lemma: left-right-inverse-unique
∀[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x y]. ∀[g2:cat-arrow(C) y x].
  ∀[g1:cat-arrow(C) y x]. g1 = g2 ∈ (cat-arrow(C) y x) supposing fg1=1 supposing g2f=1
Definition: cat-isomorphism
cat-isomorphism(C;x;y;f) ==  ∃g:cat-arrow(C) y x. (fg=1 ∧ gf=1)
Lemma: cat-isomorphism_wf
∀[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x y].  (cat-isomorphism(C;x;y;f) ∈ ℙ)
Lemma: cat-inverse-unique
∀[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x y]. ∀[g2,g1:cat-arrow(C) y x].
  (g1 = g2 ∈ (cat-arrow(C) y x)) supposing ((∃h:cat-arrow(C) y x. hf=1) and fg2=1 and fg1=1)
Lemma: cat-id-isomorphism
∀C:SmallCategory. ∀x:cat-ob(C).  cat-isomorphism(C;x;x;cat-id(C) x)
Lemma: cat-comp-isomorphism
∀C:SmallCategory. ∀a,b,c:cat-ob(C). ∀f:cat-arrow(C) a b. ∀g:cat-arrow(C) b c.
  (cat-isomorphism(C;a;b;f) 
⇒ cat-isomorphism(C;b;c;g) 
⇒ cat-isomorphism(C;a;c;cat-comp(C) a b c f g))
Definition: cat-isomorphic
cat-isomorphic(C;x;y) ==  ∃f:cat-arrow(C) x y. cat-isomorphism(C;x;y;f)
Lemma: cat-isomorphic_wf
∀[C:SmallCategory]. ∀[x,y:cat-ob(C)].  (cat-isomorphic(C;x;y) ∈ ℙ)
Lemma: cat-isomorphic_weakening
∀C:SmallCategory. ∀x,y:cat-ob(C).  cat-isomorphic(C;x;y) supposing x = y ∈ cat-ob(C)
Lemma: cat-isomorphic_inversion
∀C:SmallCategory. ∀a,b:cat-ob(C).  (cat-isomorphic(C;a;b) 
⇒ cat-isomorphic(C;b;a))
Lemma: cat-isomorphic_transitivity
∀C:SmallCategory. ∀a,b,c:cat-ob(C).  (cat-isomorphic(C;a;b) 
⇒ cat-isomorphic(C;b;c) 
⇒ cat-isomorphic(C;a;c))
Lemma: cat-isomorphic-equiv
∀C:SmallCategory. EquivRel(cat-ob(C);x,y.cat-isomorphic(C;x;y))
Definition: cat-monic
monic(f) ==
  ∀[x:cat-ob(C)]. ∀[g,h:cat-arrow(C) x y].
    g = h ∈ (cat-arrow(C) x y) supposing (cat-comp(C) x y z g f) = (cat-comp(C) x y z h f) ∈ (cat-arrow(C) x z)
Lemma: cat-monic_wf
∀[C:SmallCategory]. ∀[y,z:cat-ob(C)]. ∀[f:cat-arrow(C) y z].  (monic(f) ∈ ℙ)
Lemma: co-retraction-monic
∀[C:SmallCategory]. ∀[y,z:cat-ob(C)]. ∀[f:cat-arrow(C) y z].  monic(f) supposing co-retraction(f)
Definition: cat-epic
epic(f) ==
  ∀[z:cat-ob(C)]. ∀[g,h:cat-arrow(C) y z].
    g = h ∈ (cat-arrow(C) y z) supposing (cat-comp(C) x y z f g) = (cat-comp(C) x y z f h) ∈ (cat-arrow(C) x z)
Lemma: cat-epic_wf
∀[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x y].  (epic(f) ∈ ℙ)
Lemma: retraction-epic
∀[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x y].  epic(f) supposing retraction(f)
Definition: cat-initial
Initial(i) ==  ∀[x:cat-ob(C)]. ((∀[f,g:cat-arrow(C) i x].  (f = g ∈ (cat-arrow(C) i x))) ∧ (cat-arrow(C) i x))
Lemma: cat-initial_wf
∀[C:SmallCategory]. ∀[i:cat-ob(C)].  (Initial(i) ∈ ℙ)
Lemma: cat-initial-isomorphic
∀[C:SmallCategory]. ∀i1,i2:cat-ob(C).  (Initial(i1) 
⇒ Initial(i2) 
⇒ cat-isomorphic(C;i1;i2))
Definition: cat-final
Final(fnl) ==  ∀[x:cat-ob(C)]. ((∀[f,g:cat-arrow(C) x fnl].  (f = g ∈ (cat-arrow(C) x fnl))) ∧ (cat-arrow(C) x fnl))
Lemma: cat-final_wf
∀[C:SmallCategory]. ∀[fnl:cat-ob(C)].  (Final(fnl) ∈ ℙ)
Lemma: cat-final-isomorphic
∀[C:SmallCategory]. ∀fnl1,fnl2:cat-ob(C).  (Final(fnl1) 
⇒ Final(fnl2) 
⇒ cat-isomorphic(C;fnl1;fnl2))
Definition: cat-functor
Functor(C1;C2) ==
  {FM:F:cat-ob(C1) ⟶ cat-ob(C2)
   × (x:cat-ob(C1) ⟶ y:cat-ob(C1) ⟶ (cat-arrow(C1) x y) ⟶ (cat-arrow(C2) (F x) (F y)))| 
   let F,M = FM 
   in (∀x:cat-ob(C1). ((M x x (cat-id(C1) x)) = (cat-id(C2) (F x)) ∈ (cat-arrow(C2) (F x) (F x))))
      ∧ (∀x,y,z:cat-ob(C1). ∀f:cat-arrow(C1) x y. ∀g:cat-arrow(C1) y z.
           ((M x z (cat-comp(C1) x y z f g))
           = (cat-comp(C2) (F x) (F y) (F z) (M x y f) (M y z g))
           ∈ (cat-arrow(C2) (F x) (F z))))} 
Lemma: cat-functor_wf
∀[C1,C2:SmallCategory].  (Functor(C1;C2) ∈ Type)
Definition: mk-functor
functor(ob(a) = ob[a];arrow(x,y,f) = arrow[x; y; f]) ==  <λa.ob[a], λx,y,f. arrow[x; y; f]>
Lemma: mk-functor_wf
∀[A,B:SmallCategory]. ∀[F:cat-ob(A) ⟶ cat-ob(B)]. ∀[M:x:cat-ob(A)
                                                       ⟶ y:cat-ob(A)
                                                       ⟶ (cat-arrow(A) x y)
                                                       ⟶ (cat-arrow(B) F[x] F[y])].
  (functor(ob(a) = F[a];
           arrow(x,y,f) = M[x;y;f]) ∈ Functor(A;B)) supposing 
     ((∀x:cat-ob(A). (M[x;x;cat-id(A) x] = (cat-id(B) (F x)) ∈ (cat-arrow(B) (F x) (F x)))) and 
     (∀x,y,z:cat-ob(A). ∀f:cat-arrow(A) x y. ∀g:cat-arrow(A) y z.
        (M[x;z;cat-comp(A) x y z f g]
        = (cat-comp(B) (F x) (F y) (F z) M[x;y;f] M[y;z;g])
        ∈ (cat-arrow(B) (F x) (F z)))))
Definition: functor-ob
ob(F) ==  fst(F)
Lemma: functor-ob_wf
∀[C,D:SmallCategory]. ∀[F:Functor(C;D)].  (ob(F) ∈ cat-ob(C) ⟶ cat-ob(D))
Lemma: ob_mk_functor_lemma
∀t,arrow,ob:Top.  (functor(ob(x) = ob[x];arrow(u,v,f) = arrow[u;v;f]) t ~ ob[t])
Definition: functor-arrow
arrow(F) ==  snd(F)
Lemma: functor-arrow_wf
∀[C,D:SmallCategory]. ∀[F:Functor(C;D)].
  (arrow(F) ∈ x:cat-ob(C) ⟶ y:cat-ob(C) ⟶ (cat-arrow(C) x y) ⟶ (cat-arrow(D) (F x) (F y)))
Lemma: arrow_mk_functor_lemma
∀g,y,x,arrow,ob:Top.  (functor(ob(a) = ob[a];arrow(u,v,f) = arrow[u;v;f]) x y g ~ arrow[x;y;g])
Lemma: arrow_pair_lemma
∀y,x:Top.  (arrow(<x, y>) ~ y)
Definition: functor_arrow
F(f) ==  F x y f
Lemma: functor_arrow_wf
∀[C,D:SmallCategory]. ∀[F:Functor(C;D)]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x y].  (F(f) ∈ cat-arrow(D) (F x) (F y))
Lemma: ob_pair_lemma
∀y,x:Top.  (ob(<x, y>) ~ x)
Lemma: functor-arrow-id
∀[C,D:SmallCategory]. ∀[F:Functor(C;D)].
  ∀x:cat-ob(C). ((F x x (cat-id(C) x)) = (cat-id(D) (F x)) ∈ (cat-arrow(D) (F x) (F x)))
Lemma: functor-arrow-comp
∀[C,D:SmallCategory]. ∀[F:Functor(C;D)]. ∀[x,y,z:cat-ob(C)]. ∀[f:cat-arrow(C) x y]. ∀[g:cat-arrow(C) y z].
  ((F x z (cat-comp(C) x y z f g)) = (cat-comp(D) (F x) (F y) (F z) (F x y f) (F y z g)) ∈ (cat-arrow(D) (F x) (F z)))
Definition: const-functor
const-functor(A;a) ==  functor(ob(x) = a;arrow(x,y,f) = cat-id(A) a)
Lemma: const-functor_wf
∀[A,B:SmallCategory]. ∀[a:cat-ob(A)].  (const-functor(A;a) ∈ Functor(B;A))
Definition: full-faithful-functor
ff-functor(C;D;F) ==  ∀x,y:cat-ob(C).  Bij(cat-arrow(C) x y;cat-arrow(D) (F x) (F y);F x y)
Lemma: full-faithful-functor_wf
∀[C,D:SmallCategory]. ∀[F:Functor(C;D)].  (ff-functor(C;D;F) ∈ ℙ)
Definition: nat-trans
nat-trans(C;D;F;G) ==
  {trans:A:cat-ob(C) ⟶ (cat-arrow(D) (F A) (G A))| 
   ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
     ((cat-comp(D) (F A) (G A) (G B) (trans A) (G A B g))
     = (cat-comp(D) (F A) (F B) (G B) (F A B g) (trans B))
     ∈ (cat-arrow(D) (F A) (G B)))} 
Lemma: nat-trans_wf
∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)].  (nat-trans(C;D;F;G) ∈ Type)
Lemma: is-nat-trans
∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[trans:A:cat-ob(C) ⟶ (cat-arrow(D) (F A) (G A))].
  trans ∈ nat-trans(C;D;F;G) 
  supposing ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
              ((cat-comp(D) (F A) (G A) (G B) (trans A) (G A B g))
              = (cat-comp(D) (F A) (F B) (G B) (F A B g) (trans B))
              ∈ (cat-arrow(D) (F A) (G B)))
Lemma: nat-trans-equation
∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[T:nat-trans(C;D;F;G)]. ∀[A,B:cat-ob(C)]. ∀[g:cat-arrow(C) A B].
  ((cat-comp(D) (F A) (G A) (G B) (T A) (G A B g))
  = (cat-comp(D) (F A) (F B) (G B) (F A B g) (T B))
  ∈ (cat-arrow(D) (F A) (G B)))
Lemma: nat-trans-assoc-equation
∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[T:nat-trans(C;D;F;G)]. ∀[A,B,B':cat-ob(C)]. ∀[g:cat-arrow(C) A B].
∀[h:cat-arrow(C) B B'].
  ((cat-comp(D) (F A) (G B) (G B') (cat-comp(D) (F A) (F B) (G B) (F A B g) (T B)) (G B B' h))
  = (cat-comp(D) (F A) (F B') (G B') (cat-comp(D) (F A) (F B) (F B') (F A B g) (F B B' h)) (T B'))
  ∈ (cat-arrow(D) (F A) (G B')))
Lemma: nat-trans-comp-equation2
∀[C,D,E:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[J:Functor(D;E)]. ∀[tFG:nat-trans(C;D;F;G)]. ∀[A,B:cat-ob(C)].
∀[g:cat-arrow(C) A B]. ∀[v:cat-ob(E)].
  ((cat-comp(E) (J (F A)) (J (G B)) v 
    (cat-comp(E) (J (F A)) (J (G A)) (J (G B)) (J (F A) (G A) (tFG A)) (J (G A) (G B) (G A B g))))
  = (cat-comp(E) (J (F A)) (J (G B)) v 
     (cat-comp(E) (J (F A)) (J (F B)) (J (G B)) (J (F A) (F B) (F A B g)) (J (F B) (G B) (tFG B))))
  ∈ ((cat-arrow(E) (J (G B)) v) ⟶ (cat-arrow(E) (J (F A)) v)))
Lemma: nat-trans-equal
∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[A:nat-trans(C;D;F;G)]. ∀[B:A:cat-ob(C) ⟶ (cat-arrow(D) (F A) (G A))].
  A = B ∈ nat-trans(C;D;F;G) supposing A = B ∈ (A:cat-ob(C) ⟶ (cat-arrow(D) (F A) (G A)))
Lemma: nat-trans-equal2
∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[A,B:nat-trans(C;D;F;G)].
  A = B ∈ nat-trans(C;D;F;G) supposing A = B ∈ (A:cat-ob(C) ⟶ (cat-arrow(D) (F A) (G A)))
Definition: mk-nat-trans
x |→ T[x] ==  λx.T[x]
Lemma: mk-nat-trans_wf
∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[trans:A:cat-ob(C) ⟶ (cat-arrow(D) (F A) (G A))].
  x |→ trans[x] ∈ nat-trans(C;D;F;G) 
  supposing ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
              ((cat-comp(D) (F A) (G A) (G B) trans[A] (G A B g))
              = (cat-comp(D) (F A) (F B) (G B) (F A B g) trans[B])
              ∈ (cat-arrow(D) (F A) (G B)))
Lemma: ap_mk_nat_trans_lemma
∀z,T:Top.  (b |→ T[b] z ~ T[z])
Definition: identity-trans
identity-trans(C;D;F) ==  A |→ cat-id(D) (F A)
Lemma: identity-trans_wf
∀[C,D:SmallCategory]. ∀[F:Functor(C;D)].  (identity-trans(C;D;F) ∈ nat-trans(C;D;F;F))
Lemma: ident_trans_ap_lemma
∀A,F,D,C:Top.  (identity-trans(C;D;F) A ~ cat-id(D) (F A))
Definition: trans-comp
t1 o t2 ==  A |→ cat-comp(D) (F A) (G A) (H A) (t1 A) (t2 A)
Lemma: trans-comp_wf
∀[C,D:SmallCategory]. ∀[F,G,H:Functor(C;D)]. ∀[t1:nat-trans(C;D;F;G)]. ∀[t2:nat-trans(C;D;G;H)].
  (t1 o t2 ∈ nat-trans(C;D;F;H))
Lemma: trans_comp_ap_lemma
∀A,t2,t1,H,G,F,D,C:Top.  (t1 o t2 A ~ cat-comp(D) (F A) (G A) (H A) (t1 A) (t2 A))
Lemma: trans-id-property
∀C1,C2:SmallCategory. ∀x,y:Functor(C1;C2). ∀f:nat-trans(C1;C2;x;y).
  ((identity-trans(C1;C2;x) o f = f ∈ nat-trans(C1;C2;x;y)) ∧ (f o identity-trans(C1;C2;y) = f ∈ nat-trans(C1;C2;x;y)))
Lemma: trans-comp-assoc
∀C1,C2:SmallCategory. ∀x,y,z,w:Functor(C1;C2). ∀f:nat-trans(C1;C2;x;y). ∀g:nat-trans(C1;C2;y;z).
∀h:nat-trans(C1;C2;z;w).
  (f o g o h = f o g o h ∈ nat-trans(C1;C2;x;w))
Lemma: nat-trans-comp-equation
∀[C,D:SmallCategory]. ∀[F,G,H:Functor(C;D)]. ∀[t1:nat-trans(C;D;F;G)]. ∀[t2:nat-trans(C;D;G;H)]. ∀[A,B:cat-ob(C)].
∀[g:cat-arrow(C) A B].
  ((cat-comp(D) (F A) (H A) (H B) (cat-comp(D) (F A) (G A) (H A) (t1 A) (t2 A)) (H A B g))
  = (cat-comp(D) (F A) (F B) (H B) (F A B g) (cat-comp(D) (F B) (G B) (H B) (t1 B) (t2 B)))
  ∈ (cat-arrow(D) (F A) (H B)))
Lemma: nat-trans-assoc-comp-equation
∀[C,D:SmallCategory]. ∀[F,G,H:Functor(C;D)]. ∀[t1:nat-trans(C;D;F;H)]. ∀[t2:nat-trans(C;D;H;G)]. ∀[A,B,B':cat-ob(C)].
∀[g:cat-arrow(C) A B]. ∀[h:cat-arrow(C) B B'].
  ((cat-comp(D) (F A) (G B) (G B') 
    (cat-comp(D) (F A) (F B) (G B) (F A B g) (cat-comp(D) (F B) (H B) (G B) (t1 B) (t2 B))) 
    (G B B' h))
  = (cat-comp(D) (F A) (F B') (G B') (cat-comp(D) (F A) (F B) (F B') (F A B g) (F B B' h)) 
     (cat-comp(D) (F B') (H B') (G B') (t1 B') (t2 B')))
  ∈ (cat-arrow(D) (F A) (G B')))
Definition: functor-cat
FUN(C1;C2) ==  <Functor(C1;C2), λF,G. nat-trans(C1;C2;F;G), λF.identity-trans(C1;C2;F), λF,G,H,t1,t2. t1 o t2>
Lemma: functor-cat_wf
∀[C1,C2:SmallCategory].  (FUN(C1;C2) ∈ SmallCategory)
Lemma: functor_cat_ob_lemma
∀B,A:Top.  (cat-ob(FUN(A;B)) ~ Functor(A;B))
Lemma: functor_cat_arrow_lemma
∀G,F,B,A:Top.  (cat-arrow(FUN(A;B)) F G ~ nat-trans(A;B;F;G))
Lemma: functor_cat_id_lemma
∀F,B,A:Top.  (cat-id(FUN(A;B)) F ~ identity-trans(A;B;F))
Lemma: functor_cat_comp_lemma
∀t2,t1,H,G,F,B,A:Top.  (cat-comp(FUN(A;B)) F G H t1 t2 ~ t1 o t2)
Definition: op-cat
op-cat(C) ==  let ob,arrow,id,comp = C in <ob, λx,y. (arrow y x), id, λx,y,z,f,g. (comp z y x g f)>  
Lemma: op-cat_wf
∀[C:SmallCategory]. (op-cat(C) ∈ SmallCategory)
Lemma: op-op-cat
∀[C:SmallCategory]. (op-cat(op-cat(C)) = C ∈ SmallCategory)
Lemma: cat_ob_op_lemma
∀C:SmallCategory. (cat-ob(op-cat(C)) ~ cat-ob(C))
Lemma: op-cat-arrow
∀C:SmallCategory. ∀[A,B:Top].  (cat-arrow(op-cat(C)) A B ~ cat-arrow(C) B A)
Lemma: op-cat-comp
∀C:SmallCategory. ∀[I,J,K,f,g:Top].  (cat-comp(op-cat(C)) I J K f g ~ cat-comp(C) K J I g f)
Lemma: op-cat-id
∀C:SmallCategory. ∀[A:Top]. (cat-id(op-cat(C)) A ~ cat-id(C) A)
Definition: op-functor
op-functor(F) ==  functor(ob(x) = F x;arrow(a,b,f) = F b a f)
Lemma: op-functor_wf
∀[C,D:SmallCategory]. ∀[F:Functor(C;D)].  (op-functor(F) ∈ Functor(op-cat(C);op-cat(D)))
Definition: type-cat
TypeCat ==  <Type, λI,J. (I ⟶ J), λI,x. x, λI,J,K,f,g. (g o f)>
Lemma: type-cat_wf
TypeCat ∈ SmallCategory'
Lemma: void-initial-type
Initial(Void)
Lemma: top-final-type
Final(Top)
Definition: presheaf-cat
Presheafs(C) ==  FUN(op-cat(C);TypeCat)
Lemma: presheaf-cat_wf
∀[C:SmallCategory]. (Presheafs(C) ∈ SmallCategory')
Definition: presheaf
Presheaf(C) ==  Functor(op-cat(C);TypeCat)
Lemma: presheaf_wf
∀[C:SmallCategory]. (Presheaf(C) ∈ 𝕌')
Definition: ext-equal-presheaves
ext-equal-presheaves(C;F;G) ==
  (∀x:cat-ob(C). F x ≡ G x) ∧ (∀x,y:cat-ob(C). ∀f:cat-arrow(C) y x.  ((F x y f) = (G x y f) ∈ ((F x) ⟶ (F y))))
Lemma: ext-equal-presheaves_wf
∀[C:SmallCategory]. ∀[F,G:Presheaf(C)].  (ext-equal-presheaves(C;F;G) ∈ ℙ')
Lemma: ext-equal-presheaves-equiv-rel
∀[C:SmallCategory]. EquivRel(Presheaf(C);F,G.ext-equal-presheaves(C;F;G))
Definition: mk-presheaf
Presheaf(Set(I) =S[I];
         Morphism(I,J,f,rho) = morph[I; J; f; rho]) ==
  functor(ob(I) = S[I];
          arrow(I,J,f) = λrho.morph[I; J; f; rho])
Lemma: mk-presheaf_wf
∀[C:SmallCategory]. ∀[S:cat-ob(C) ⟶ Type]. ∀[morph:I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ S[I] ⟶ S[J]].
  (Presheaf(Set(I) =S[I];
            Morphism(I,J,f,rho) = morph[I;J;f;rho]) ∈ Presheaf(C)) supposing 
     ((∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀rho:S[I].
         (morph[I;K;cat-comp(C) K J I g f;rho] = morph[J;K;g;morph[I;J;f;rho]] ∈ S[K])) and 
     (∀I:cat-ob(C). ∀rho:S[I].  (morph[I;I;cat-id(C) I;rho] = rho ∈ S[I])))
Definition: rep-pre-sheaf
rep-pre-sheaf(C;X) ==  <λU.(cat-arrow(C) U X), λU,U',f,ux. (cat-comp(C) U' U X f ux)>
Lemma: rep-pre-sheaf_wf
∀[C:SmallCategory]. ∀[X:cat-ob(C)].  (rep-pre-sheaf(C;X) ∈ Functor(op-cat(C);TypeCat))
Definition: rep-sub-sheaf
rep-sub-sheaf(C;X;P) ==  <λU.{f:cat-arrow(C) U X| P U f} , λU,U',f,ux. (cat-comp(C) U' U X f ux)>
Lemma: rep-sub-sheaf_wf
∀[C:SmallCategory]. ∀[X:cat-ob(C)]. ∀[P:U:cat-ob(C) ⟶ (cat-arrow(C) U X) ⟶ ℙ].
  rep-sub-sheaf(C;X;P) ∈ Functor(op-cat(C);TypeCat) 
  supposing ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B. ∀b:{b:cat-arrow(C) B X| P B b} .  (P A (cat-comp(C) A B X g b))
Definition: yoneda-embedding
yoneda-embedding(C) ==  functor(ob(X) = rep-pre-sheaf(C;X);arrow(X,Y,f) = A |→ λg.(cat-comp(C) A X Y g f))
Lemma: yoneda-embedding_wf
∀[C:SmallCategory]. (yoneda-embedding(C) ∈ Functor(C;FUN(op-cat(C);TypeCat)))
Lemma: yoneda-lemma
∀C:SmallCategory. ff-functor(C;FUN(op-cat(C);TypeCat);yoneda-embedding(C))
Definition: functor-comp
functor-comp(F;G) ==  functor(ob(x) = G (F x);arrow(x,y,a) = G (F x) (F y) (F x y a))
Lemma: functor-comp_wf
∀[A,B,C:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;C)].  (functor-comp(F;G) ∈ Functor(A;C))
Lemma: equal-functors1
∀[A,B:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:F:cat-ob(A) ⟶ cat-ob(B) × (x:cat-ob(A)
                                                                        ⟶ y:cat-ob(A)
                                                                        ⟶ (cat-arrow(A) x y)
                                                                        ⟶ (cat-arrow(B) (F x) (F y)))].
  (F = G ∈ Functor(A;B)) supposing 
     ((∀x,y:cat-ob(A). ∀f:cat-arrow(A) x y.  ((F x y f) = ((snd(G)) x y f) ∈ (cat-arrow(B) (F x) (F y)))) and 
     (∀x:cat-ob(A). ((F x) = ((fst(G)) x) ∈ cat-ob(B))))
Lemma: equal-functors
∀[A,B:SmallCategory]. ∀[F,G:Functor(A;B)].
  (F = G ∈ Functor(A;B)) supposing 
     ((∀x,y:cat-ob(A). ∀f:cat-arrow(A) x y.  ((F x y f) = (G x y f) ∈ (cat-arrow(B) (F x) (F y)))) and 
     (∀x:cat-ob(A). ((F x) = (G x) ∈ cat-ob(B))))
Lemma: equal-presheaves
∀[C:SmallCategory]. ∀[F,G:Presheaf(C)].
  F = G ∈ Presheaf(C) 
  supposing (∀x:cat-ob(op-cat(C)). ((F x) = (G x) ∈ cat-ob(TypeCat)))
  ∧ (∀x,y:cat-ob(op-cat(C)). ∀f:cat-arrow(op-cat(C)) x y.  ((F x y f) = (G x y f) ∈ (cat-arrow(TypeCat) (F x) (F y))))
Lemma: functor-comp-assoc
∀[A,B,C,D:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;C)]. ∀[H:Functor(C;D)].
  (functor-comp(F;functor-comp(G;H)) = functor-comp(functor-comp(F;G);H) ∈ Functor(A;D))
Definition: id_functor
1 ==  functor(ob(x) = x;arrow(x,y,a) = a)
Lemma: id_functor_wf
∀[A:SmallCategory]. (1 ∈ Functor(A;A))
Lemma: functor-comp-id
∀[A,B:SmallCategory]. ∀[F:Functor(A;B)].
  ((functor-comp(F;1) = F ∈ Functor(A;B)) ∧ (functor-comp(1;F) = F ∈ Functor(A;B)))
Lemma: unit-functor-is-const
∀[A:SmallCategory]. ∀f:Functor(1;A). ∃a:cat-ob(A). (f = const-functor(A;a) ∈ Functor(1;A))
Definition: cat-cat
Cat ==  <SmallCategory, λC1,C2. Functor(C1;C2), λC.1, λC1,C2,C3,F,G. functor-comp(F;G)>
Lemma: cat-cat_wf
Cat ∈ SmallCategory'
Lemma: functor-is-isomorphism
∀[A,B:SmallCategory].
  ∀f:Functor(A;B)
    (cat-isomorphism(Cat;A;B;f)
    
⇐⇒ Bij(cat-ob(A);cat-ob(B);ob(f)) ∧ (∀x,y:cat-ob(A).  Bij(cat-arrow(A) x y;cat-arrow(B) (f x) (f y);f x y)))
Definition: product-cat
A × B ==
  <cat-ob(A) × cat-ob(B)
  , λxy,uv. (cat-arrow(A) (fst(xy)) (fst(uv)) × (cat-arrow(B) (snd(xy)) (snd(uv))))
  , λxy.<cat-id(A) (fst(xy)), cat-id(B) (snd(xy))>
  , λxy,uv,wz,F,G. <cat-comp(A) (fst(xy)) (fst(uv)) (fst(wz)) (fst(F)) (fst(G))
                   , cat-comp(B) (snd(xy)) (snd(uv)) (snd(wz)) (snd(F)) (snd(G))
                   >>
Lemma: product-cat_wf
∀[A,B:SmallCategory].  (A × B ∈ SmallCategory)
Lemma: ob_product_lemma
∀B,A:Top.  (cat-ob(A × B) ~ cat-ob(A) × cat-ob(B))
Lemma: arrow_prod_lemma
∀y,x,B,A:Top.  (cat-arrow(A × B) x y ~ cat-arrow(A) (fst(x)) (fst(y)) × (cat-arrow(B) (snd(x)) (snd(y))))
Lemma: id_prod_cat_lemma
∀x,B,A:Top.  (cat-id(A × B) x ~ <cat-id(A) (fst(x)), cat-id(B) (snd(x))>)
Lemma: comp_product_cat_lemma
∀g,f,z,y,x,B,A:Top.
  (cat-comp(A × B) x y z f g ~ <cat-comp(A) (fst(x)) (fst(y)) (fst(z)) (fst(f)) (fst(g))
                               , cat-comp(B) (snd(x)) (snd(y)) (snd(z)) (snd(f)) (snd(g))
                               >)
Lemma: functor-arrow-prod-id
∀[A,B,C:SmallCategory]. ∀[F:Functor(A × B;C)]. ∀[a:cat-ob(A)]. ∀[b:cat-ob(B)].
  ((F <a, b> <a, b> <cat-id(A) a, cat-id(B) b>) = (cat-id(C) (F <a, b>)) ∈ (cat-arrow(C) (F <a, b>) (F <a, b>)))
Lemma: functor-arrow-prod-comp
∀[A,B,C:SmallCategory]. ∀[F:Functor(A × B;C)]. ∀[a1,a2,a3:cat-ob(A)]. ∀[f:cat-arrow(A) a1 a2]. ∀[g:cat-arrow(A) a2 a3].
∀[b1,b2,b3:cat-ob(B)]. ∀[h:cat-arrow(B) b1 b2]. ∀[k:cat-arrow(B) b2 b3].
  ((cat-comp(C) (F <a1, b1>) (F <a2, b2>) (F <a3, b3>) (F <a1, b1> <a2, b2> <f, h>) (F <a2, b2> <a3, b3> <g, k>))
  = (F <a1, b1> <a3, b3> <cat-comp(A) a1 a2 a3 f g, cat-comp(B) b1 b2 b3 h k>)
  ∈ (cat-arrow(C) (F <a1, b1>) (F <a3, b3>)))
Definition: trans-horizontal-comp
trans-horizontal-comp(E;F;G;J;K;tFG;tJK) ==
  x |→ cat-comp(E) (J (F x)) (K (F x)) (K (G x)) (tJK (F x)) (K (F x) (G x) (tFG x))
Lemma: trans-horizontal-comp_wf
∀[C,D,E:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[J,K:Functor(D;E)]. ∀[tFG:nat-trans(C;D;F;G)]. ∀[tJK:nat-trans(D;E;J;K)].
  (trans-horizontal-comp(E;F;G;J;K;tFG;tJK) ∈ nat-trans(C;E;functor-comp(F;J);functor-comp(G;K)))
Lemma: trans-exchange
∀[C,D,E:SmallCategory]. ∀[F,G,H:Functor(C;D)]. ∀[I,J,K:Functor(D;E)]. ∀[tFG:nat-trans(C;D;F;G)].
∀[tGH:nat-trans(C;D;G;H)]. ∀[tIJ:nat-trans(D;E;I;J)]. ∀[tJK:nat-trans(D;E;J;K)].
  (trans-horizontal-comp(E;F;G;I;J;tFG;tIJ) o trans-horizontal-comp(E;G;H;J;K;tGH;tJK)
  = trans-horizontal-comp(E;F;H;I;K;tFG o tGH;tIJ o tJK)
  ∈ nat-trans(C;E;functor-comp(F;I);functor-comp(H;K)))
Definition: functor-curry
functor-curry(A;B) ==
  functor(ob(F) = functor(ob(a) = functor(ob(b) = F <a, b>
                                          arrow(x,y,f) = F <a, x> <a, y> <cat-id(A) a, f>);
                          arrow(x,y,f) = b |→ F <x, b> <y, b> <f, cat-id(B) b>);
          arrow(F,G,T) = a |→ b |→ T <a, b>)
Lemma: functor-curry_wf
∀[A,B,C:SmallCategory].  (functor-curry(A;B) ∈ Functor(FUN(A × B;C);FUN(A;FUN(B;C))))
Definition: functor-uncurry
functor-uncurry(C) ==
  functor(ob(f) = functor(ob(p) = f (fst(p)) (snd(p));
                          arrow(x,y,p) = cat-comp(C) (f (fst(x)) (snd(x))) (f (fst(y)) (snd(x))) (f (fst(y)) (snd(y))) 
                                         (f (fst(x)) (fst(y)) (fst(p)) (snd(x))) 
                                         (f (fst(y)) (snd(x)) (snd(y)) (snd(p))));
          arrow(f,g,T) = ab |→ T (fst(ab)) (snd(ab)))
Lemma: functor-uncurry_wf
∀[A,B,C:SmallCategory].  (functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C)))
Lemma: functor-curry-iso
∀A,B,C:SmallCategory.  cat-isomorphic(Cat;FUN(A × B;C);FUN(A;FUN(B;C)))
Definition: cat-square-commutes
x_y1 o y1_z = x_y2 o y2_z ==  (cat-comp(C) x y1 z x_y1 y1_z) = (cat-comp(C) x y2 z x_y2 y2_z) ∈ (cat-arrow(C) x z)
Lemma: cat-square-commutes_wf
∀[C:SmallCategory]. ∀[x,y1,y2,z:cat-ob(C)]. ∀[x_y1:cat-arrow(C) x y1]. ∀[y1_z:cat-arrow(C) y1 z]. ∀[x_y2:cat-arrow(C) x 
                                                                                                         y2].
∀[y2_z:cat-arrow(C) y2 z].
  (x_y1 o y1_z = x_y2 o y2_z ∈ ℙ)
Lemma: cat-square-commutes-sym
∀[C:SmallCategory]. ∀[x,y1,y2,z:cat-ob(C)]. ∀[x_y1:cat-arrow(C) x y1]. ∀[y1_z:cat-arrow(C) y1 z]. ∀[x_y2:cat-arrow(C) x 
                                                                                                         y2].
∀[y2_z:cat-arrow(C) y2 z].
  uiff(x_y1 o y1_z = x_y2 o y2_z;x_y2 o y2_z = x_y1 o y1_z)
Lemma: cat-square-commutes-comp
∀[C:SmallCategory]. ∀[x1,x2,x3,y1,y2,y3:cat-ob(C)]. ∀[x1_y1:cat-arrow(C) x1 y1]. ∀[x2_y2:cat-arrow(C) x2 y2].
∀[x3_y3:cat-arrow(C) x3 y3]. ∀[y1_y2:cat-arrow(C) y1 y2]. ∀[y2_y3:cat-arrow(C) y2 y3]. ∀[x1_x2:cat-arrow(C) x1 x2].
∀[x2_x3:cat-arrow(C) x2 x3].
  (x1_y1 o cat-comp(C) y1 y2 y3 y1_y2 y2_y3 = cat-comp(C) x1 x2 x3 x1_x2 x2_x3 o x3_y3) supposing 
     (x1_y1 o y1_y2 = x1_x2 o x2_y2 and 
     x2_y2 o y2_y3 = x2_x3 o x3_y3)
Definition: groupoid
Groupoid ==
  C:SmallCategory × {inv:x:cat-ob(C) ⟶ y:cat-ob(C) ⟶ (cat-arrow(C) x y) ⟶ (cat-arrow(C) y x)| 
                     ∀x,y:cat-ob(C). ∀f:cat-arrow(C) x y.
                       (((cat-comp(C) x y x f (inv x y f)) = (cat-id(C) x) ∈ (cat-arrow(C) x x))
                       ∧ ((cat-comp(C) y x y (inv x y f) f) = (cat-id(C) y) ∈ (cat-arrow(C) y y)))} 
Lemma: groupoid_wf
Groupoid ∈ 𝕌'
Definition: groupoid-cat
cat(G) ==  fst(G)
Lemma: groupoid-cat_wf
∀[G:Groupoid]. (cat(G) ∈ SmallCategory)
Definition: groupoid-inv
groupoid-inv(G;x;y;x_y) ==  (snd(G)) x y x_y
Lemma: groupoid-inv_wf
∀[G:Groupoid]. ∀[x,y:cat-ob(cat(G))]. ∀[x_y:cat-arrow(cat(G)) x y].  (groupoid-inv(G;x;y;x_y) ∈ cat-arrow(cat(G)) y x)
Lemma: groupoid_inv
∀[G:Groupoid]
  ∀x,y:cat-ob(cat(G)). ∀f:cat-arrow(cat(G)) x y.
    (((cat-comp(cat(G)) x y x f groupoid-inv(G;x;y;f)) = (cat-id(cat(G)) x) ∈ (cat-arrow(cat(G)) x x))
    ∧ ((cat-comp(cat(G)) y x y groupoid-inv(G;x;y;f) f) = (cat-id(cat(G)) y) ∈ (cat-arrow(cat(G)) y y)))
Definition: mk-groupoid
Groupoid(C;inv(x,y,f) = inv[x; y; f]) ==  <C, λx,y,f. inv[x; y; f]>
Lemma: mk-groupoid_wf
∀[C:SmallCategory]. ∀[inv:x:cat-ob(C) ⟶ y:cat-ob(C) ⟶ (cat-arrow(C) x y) ⟶ (cat-arrow(C) y x)].
  Groupoid(C;
           inv(x,y,f) = inv[x;y;f]) ∈ Groupoid 
  supposing ∀x,y:cat-ob(C). ∀f:cat-arrow(C) x y.
              (((cat-comp(C) x y x f inv[x;y;f]) = (cat-id(C) x) ∈ (cat-arrow(C) x x))
              ∧ ((cat-comp(C) y x y inv[x;y;f] f) = (cat-id(C) y) ∈ (cat-arrow(C) y y)))
Definition: groupoid-map
groupoid-map(G;H) ==
  {F:Functor(cat(G);cat(H))| 
   ∀x,y:cat-ob(cat(G)). ∀f:cat-arrow(cat(G)) x y.
     ((F y x groupoid-inv(G;x;y;f)) = groupoid-inv(H;F x;F y;F x y f) ∈ (cat-arrow(cat(H)) (F y) (F x)))} 
Lemma: groupoid-map_wf
∀[G,H:Groupoid].  (groupoid-map(G;H) ∈ Type)
Definition: groupoids
Groupoids ==  Cat(ob = Groupoid;arrow(G,H) = groupoid-map(G;H);id(G) = 1;comp(G,H,K,F,G) = functor-comp(F;G))
Lemma: groupoids_wf
Groupoids ∈ SmallCategory'
Definition: tree-groupoid
tree-groupoid(X) ==  Groupoid(tree-cat(X);inv(x,y,f) = ⋅)
Lemma: tree-groupoid_wf
∀[X:Type]. (tree-groupoid(X) ∈ Groupoid)
Definition: discrete-groupoid
discrete-groupoid(X) ==  Groupoid(discrete-cat(X);inv(x,y,f) = ⋅)
Lemma: discrete-groupoid_wf
∀[X:Type]. (discrete-groupoid(X) ∈ Groupoid)
Definition: interval-groupoid
interval-groupoid() ==  tree-groupoid(ℕ2)
Lemma: interval-groupoid_wf
interval-groupoid() ∈ Groupoid
Lemma: groupoid-right-cancellation
∀[G:Groupoid]. ∀[x,y,z:cat-ob(cat(G))]. ∀[a,b:cat-arrow(cat(G)) x y]. ∀[c:cat-arrow(cat(G)) y z].
  uiff((cat-comp(cat(G)) x y z a c) = (cat-comp(cat(G)) x y z b c) ∈ (cat-arrow(cat(G)) x z);a
  = b
  ∈ (cat-arrow(cat(G)) x y))
Lemma: groupoid-left-cancellation
∀[G:Groupoid]. ∀[x,y,z:cat-ob(cat(G))]. ∀[a,b:cat-arrow(cat(G)) y z]. ∀[c:cat-arrow(cat(G)) x y].
  uiff((cat-comp(cat(G)) x y z c a) = (cat-comp(cat(G)) x y z c b) ∈ (cat-arrow(cat(G)) x z);a
  = b
  ∈ (cat-arrow(cat(G)) y z))
Lemma: groupoid-square-commutes-iff
∀[G:Groupoid]. ∀[x,y1,y2,z:cat-ob(cat(G))]. ∀[x_y1:cat-arrow(cat(G)) x y1]. ∀[y1_z:cat-arrow(cat(G)) y1 z].
∀[x_y2:cat-arrow(cat(G)) x y2]. ∀[y2_z:cat-arrow(cat(G)) y2 z].
  uiff(x_y1 o y1_z = x_y2 o y2_z;y2_z
  = (cat-comp(cat(G)) y2 x z groupoid-inv(G;x;y2;x_y2) (cat-comp(cat(G)) x y1 z x_y1 y1_z))
  ∈ (cat-arrow(cat(G)) y2 z))
Lemma: groupoid-square-commutes-iff2
∀[G:Groupoid]. ∀[x,y1,y2,z:cat-ob(cat(G))]. ∀[x_y1:cat-arrow(cat(G)) x y1]. ∀[y1_z:cat-arrow(cat(G)) y1 z].
∀[x_y2:cat-arrow(cat(G)) x y2]. ∀[y2_z:cat-arrow(cat(G)) y2 z].
  uiff(x_y1 o y1_z = x_y2 o y2_z;x_y1
  = (cat-comp(cat(G)) x z y1 (cat-comp(cat(G)) x y2 z x_y2 y2_z) groupoid-inv(G;y1;z;y1_z))
  ∈ (cat-arrow(cat(G)) x y1))
Lemma: groupoid-cube
∀[G:Groupoid]. ∀[x000,x100,x010,x110,x001,x101,x011,x111:cat-ob(cat(G))]. ∀[a:cat-arrow(cat(G)) x001 x011].
∀[b:cat-arrow(cat(G)) x011 x111]. ∀[c:cat-arrow(cat(G)) x001 x101]. ∀[d:cat-arrow(cat(G)) x101 x111].
∀[e:cat-arrow(cat(G)) x000 x010]. ∀[f:cat-arrow(cat(G)) x010 x110]. ∀[g:cat-arrow(cat(G)) x000 x100].
∀[h:cat-arrow(cat(G)) x100 x110]. ∀[i:cat-arrow(cat(G)) x000 x001]. ∀[j:cat-arrow(cat(G)) x010 x011].
∀[k:cat-arrow(cat(G)) x110 x111]. ∀[l:cat-arrow(cat(G)) x100 x101].
  (a o b = c o d supposing e o j = i o a ∧ f o k = j o b ∧ l o d = h o k ∧ i o c = g o l ∧ e o f = g o h
  ∧ e o j = i o a supposing a o b = c o d ∧ f o k = j o b ∧ l o d = h o k ∧ i o c = g o l ∧ e o f = g o h
  ∧ f o k = j o b supposing e o j = i o a ∧ a o b = c o d ∧ l o d = h o k ∧ i o c = g o l ∧ e o f = g o h
  ∧ l o d = h o k supposing e o j = i o a ∧ f o k = j o b ∧ a o b = c o d ∧ i o c = g o l ∧ e o f = g o h
  ∧ i o c = g o l supposing e o j = i o a ∧ f o k = j o b ∧ l o d = h o k ∧ a o b = c o d ∧ e o f = g o h
  ∧ e o f = g o h supposing e o j = i o a ∧ f o k = j o b ∧ l o d = h o k ∧ i o c = g o l ∧ a o b = c o d)
Lemma: groupoid-cube-lemma
∀[G:Groupoid]. ∀[x000,x100,x010,x110,x001,x101,x011,x111:cat-ob(cat(G))]. ∀[a:cat-arrow(cat(G)) x001 x011].
∀[b:cat-arrow(cat(G)) x011 x111]. ∀[c:cat-arrow(cat(G)) x001 x101]. ∀[d:cat-arrow(cat(G)) x101 x111].
∀[e:cat-arrow(cat(G)) x000 x010]. ∀[f:cat-arrow(cat(G)) x010 x110]. ∀[g:cat-arrow(cat(G)) x000 x100].
∀[h:cat-arrow(cat(G)) x100 x110]. ∀[i:cat-arrow(cat(G)) x000 x001]. ∀[j:cat-arrow(cat(G)) x010 x011].
∀[k:cat-arrow(cat(G)) x110 x111]. ∀[l:cat-arrow(cat(G)) x100 x101].
  uiff(a o b = c o d;e o f = g o h) supposing e o j = i o a ∧ f o k = j o b ∧ l o d = h o k ∧ i o c = g o l
Lemma: groupoid-cube-lemma-rev
∀[G:Groupoid]. ∀[x000,x100,x010,x110,x001,x101,x011,x111:cat-ob(cat(G))]. ∀[a:cat-arrow(cat(G)) x001 x011].
∀[b:cat-arrow(cat(G)) x011 x111]. ∀[c:cat-arrow(cat(G)) x001 x101]. ∀[d:cat-arrow(cat(G)) x101 x111].
∀[e:cat-arrow(cat(G)) x000 x010]. ∀[f:cat-arrow(cat(G)) x010 x110]. ∀[g:cat-arrow(cat(G)) x000 x100].
∀[h:cat-arrow(cat(G)) x100 x110]. ∀[i:cat-arrow(cat(G)) x001 x000]. ∀[j:cat-arrow(cat(G)) x011 x010].
∀[k:cat-arrow(cat(G)) x111 x110]. ∀[l:cat-arrow(cat(G)) x101 x100].
  uiff(a o b = c o d;e o f = g o h) supposing a o j = i o e ∧ b o k = j o f ∧ d o k = l o h ∧ i o g = c o l
Lemma: groupoid-cube-lemma2
∀[G:Groupoid]. ∀[x000,x100,x010,x110,x001,x101,x011,x111:cat-ob(cat(G))]. ∀[a:cat-arrow(cat(G)) x001 x011].
∀[b:cat-arrow(cat(G)) x011 x111]. ∀[c:cat-arrow(cat(G)) x001 x101]. ∀[d:cat-arrow(cat(G)) x101 x111].
∀[e:cat-arrow(cat(G)) x000 x010]. ∀[f:cat-arrow(cat(G)) x010 x110]. ∀[g:cat-arrow(cat(G)) x000 x100].
∀[h:cat-arrow(cat(G)) x100 x110].
  uiff(a o b = c o d;e o f = g o h) 
  supposing (∃i:cat-arrow(cat(G)) x000 x001
              ∃j:cat-arrow(cat(G)) x010 x011
               ∃k:cat-arrow(cat(G)) x110 x111
                ∃l:cat-arrow(cat(G)) x100 x101. (e o j = i o a ∧ f o k = j o b ∧ l o d = h o k ∧ i o c = g o l))
  ∨ (∃i:cat-arrow(cat(G)) x001 x000
      ∃j:cat-arrow(cat(G)) x011 x010
       ∃k:cat-arrow(cat(G)) x111 x110
        ∃l:cat-arrow(cat(G)) x101 x100. (a o j = i o e ∧ b o k = j o f ∧ d o k = l o h ∧ i o g = c o l))
Definition: groupoid-square1
groupoid-square1(G;x00;x10;x01;x11;a;b;c) ==
  cat-comp(cat(G)) x01 x10 x11 (cat-comp(cat(G)) x01 x00 x10 groupoid-inv(G;x00;x01;c) a) b
Lemma: groupoid-square1_wf
∀[G:Groupoid]. ∀[x00,x10,x01,x11:cat-ob(cat(G))]. ∀[a:cat-arrow(cat(G)) x00 x10]. ∀[b:cat-arrow(cat(G)) x10 x11].
∀[c:cat-arrow(cat(G)) x00 x01].
  (groupoid-square1(G;x00;x10;x01;x11;a;b;c) ∈ {d:cat-arrow(cat(G)) x01 x11| a o b = c o d} )
Definition: groupoid-square2
groupoid-square2(G;x00;x10;x01;x11;b;c;d) ==
  cat-comp(cat(G)) x00 x11 x10 (cat-comp(cat(G)) x00 x01 x11 c d) groupoid-inv(G;x10;x11;b)
Lemma: groupoid-square2_wf
∀G:Groupoid. ∀x00,x10,x01,x11:cat-ob(cat(G)). ∀d:cat-arrow(cat(G)) x01 x11. ∀b:cat-arrow(cat(G)) x10 x11.
∀c:cat-arrow(cat(G)) x00 x01.
  (groupoid-square2(G;x00;x10;x01;x11;b;c;d) ∈ {a:cat-arrow(cat(G)) x00 x10| a o b = c o d} )
Definition: comma-cat
(S ↓ T) ==
  Cat(ob = a:cat-ob(A) × b:cat-ob(B) × (cat-arrow(C) (S a) (T b));
      arrow(x,y) = let a,b,f = x in 
      let a',b',f' = y in 
      {gh:cat-arrow(A) a a' × (cat-arrow(B) b b')| 
       (cat-comp(C) (S a) (T b) (T b') f (T b b' (snd(gh))))
       = (cat-comp(C) (S a) (S a') (T b') (S a a' (fst(gh))) f')
       ∈ (cat-arrow(C) (S a) (T b'))}
      id(x) = let a,b,f = x in 
      <cat-id(A) a, cat-id(B) b>
      comp(u,v,w,fp,gp) = let a,b,x = u in 
      let a',b',x' = v in 
      let a'',b'',x'' = w in 
      let f,g = fp 
      in let f',g' = gp 
         in <cat-comp(A) a a' a'' f f', cat-comp(B) b b' b'' g g'>)
Lemma: comma-cat_wf
∀[A,B,C:SmallCategory]. ∀[S:Functor(A;C)]. ∀[T:Functor(B;C)].  ((S ↓ T) ∈ SmallCategory)
Definition: arrow-cat
arrow-cat(C) ==  (1 ↓ 1)
Lemma: arrow-cat_wf
∀[C:SmallCategory]. (arrow-cat(C) ∈ SmallCategory)
Definition: comma-slice-cat
(S ↓ x) ==  (S ↓ const-functor(C;x))
Lemma: comma-slice-cat_wf
∀[A,C:SmallCategory]. ∀[S:Functor(A;C)]. ∀[x:cat-ob(C)].  ((S ↓ x) ∈ SmallCategory)
Definition: slice-cat
(C ↓ b) ==  (1 ↓ b)
Lemma: slice-cat_wf
∀[C:SmallCategory]. ∀[x:cat-ob(C)].  ((C ↓ x) ∈ SmallCategory)
Definition: comma-coslice-cat
(x ↓ T) ==  (const-functor(C;x) ↓ T)
Lemma: comma-coslice-cat_wf
∀[B,C:SmallCategory]. ∀[T:Functor(B;C)]. ∀[x:cat-ob(C)].  ((x ↓ T) ∈ SmallCategory)
Definition: coslice-cat
(b ↓ C) ==  (b ↓ 1)
Lemma: coslice-cat_wf
∀[C:SmallCategory]. ∀[x:cat-ob(C)].  ((x ↓ C) ∈ SmallCategory)
Definition: group-cat
Group ==  Cat(ob = Group{i};arrow(G,H) = MonHom(G,H);id(G) = λx.x;comp(G,H,K,f,g) = g o f)
Lemma: group-cat_wf
Group ∈ SmallCategory'
Definition: presheaf-elements
el(P) ==
  Cat(ob = A:cat-ob(op-cat(C)) × (P A);
      arrow(Aa,Bb) = let A,a = Aa 
                     in let B,b = Bb 
                        in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)}
      id(Aa) = cat-id(op-cat(C)) (fst(Aa));
      comp(Aa,Bb,Dd,f,g) = cat-comp(op-cat(C)) (fst(Dd)) (fst(Bb)) (fst(Aa)) g f)
Lemma: presheaf-elements-sq
∀C:SmallCategory. ∀P:Top.
  (el(P) ~ Cat(ob = A:cat-ob(C) × (P A);
               arrow(Aa,Bb) = let A,a = Aa 
                              in let B,b = Bb 
                                 in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)}
               id(Aa) = cat-id(C) (fst(Aa));
               comp(Aa,Bb,Dd,f,g) = cat-comp(C) (fst(Aa)) (fst(Bb)) (fst(Dd)) f g))
Lemma: presheaf-elements_wf
∀C:SmallCategory. ∀P:Presheaf(C).  (el(P) ∈ SmallCategory)
Definition: stable-element-predicate
stable-element-predicate(C;F;I,rho.P[I; rho]) ==
  ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀rho:F I.  (P[I; rho] 
⇒ P[J; F I J f rho])
Lemma: stable-element-predicate_wf
∀[C:SmallCategory]. ∀[F:Presheaf(C)]. ∀[P:I:cat-ob(C) ⟶ (F I) ⟶ ℙ].
  (stable-element-predicate(C;F;I,rho.P[I;rho]) ∈ ℙ)
Definition: presheaf-subset
F|I,rho.P[I; rho] ==  Presheaf(Set(I) ={rho:F I| P[I; rho]} Morphism(I,J,f,rho) = F I J f rho)
Lemma: presheaf-subset_wf
∀[C:SmallCategory]. ∀[F:Presheaf(C)]. ∀[P:I:cat-ob(C) ⟶ (F I) ⟶ ℙ].
  F|I,rho.P[I;rho] ∈ Presheaf(C) supposing stable-element-predicate(C;F;I,rho.P[I;rho])
Lemma: presheaf-subset-true
∀[C:SmallCategory]. ∀[F:Presheaf(C)].  ext-equal-presheaves(C;F|True;F)
Lemma: presheaf-subset-and
∀[C:SmallCategory]. ∀[F:Presheaf(C)]. ∀[P,Q:I:cat-ob(C) ⟶ (F I) ⟶ ℙ].
  ext-equal-presheaves(C;F|I,rho.P[I;rho]|I,rho.Q[I;rho];F|I,rho.P[I;rho] ∧ Q[I;rho]) 
  supposing stable-element-predicate(C;F;I,rho.P[I;rho]) ∧ stable-element-predicate(C;F;I,rho.Q[I;rho])
Definition: presheaf_map
A ⟶ B ==  nat-trans(op-cat(C);TypeCat;A;B)
Lemma: presheaf_map_wf
∀[C:SmallCategory]. ∀[A,B:Presheaf(C)].  (A ⟶ B ∈ 𝕌')
Definition: presheaf-element-map
presheaf-element-map(m) ==  functor(ob(p) = let I,a = p in <I, m I a>arrow(p,q,f) = f)
Lemma: presheaf-element-map_wf
∀[C:SmallCategory]. ∀[A,B:Presheaf(C)]. ∀[m:A ⟶ B].  (presheaf-element-map(m) ∈ Functor(el(A);el(B)))
Definition: functor-presheaf
functor-presheaf(F;P) ==  functor-comp(op-functor(F);P)
Lemma: functor-presheaf_wf
∀[C,D:SmallCategory].  ∀F:Functor(C;D). ∀P:Presheaf(D).  (functor-presheaf(F;P) ∈ Presheaf(C))
Definition: distributive-lattice-cat
BddDistributiveLattice ==
  Cat(ob = BoundedDistributiveLattice;
      arrow(G,H) = Hom(G;H);
      id(G) = λx.x;
      comp(G,H,K,f,g) = g o f)
Lemma: distributive-lattice-cat_wf
BddDistributiveLattice ∈ SmallCategory'
Definition: free-group-functor
FreeGp ==  functor(ob(X) = free-group(X);arrow(X,Y,f) = fg-lift(free-group(Y);λx.free-letter(f x)))
Lemma: free-group-functor_wf
FreeGp ∈ Functor(TypeCat;Group)
Definition: free-dl-functor
FreeDistLattice ==  functor(ob(X) = free-dl(X);arrow(X,Y,f) = fdl-hom(free-dl(Y);λx.free-dl-generator(f x)))
Lemma: free-dl-functor_wf
FreeDistLattice ∈ Functor(TypeCat;BddDistributiveLattice)
Definition: forget-group
ForgetGroup ==  functor(ob(G) = |G|;arrow(G,H,f) = f)
Lemma: forget-group_wf
ForgetGroup ∈ Functor(Group;TypeCat)
Definition: forget-lattice
ForgetLattice ==  functor(ob(ltt) = Point(ltt);arrow(G,H,f) = f)
Lemma: forget-lattice_wf
ForgetLattice ∈ Functor(BddDistributiveLattice;TypeCat)
Definition: counit-unit-equations
counit-unit-equations(D;C;F;G;eps;eta) ==
  (∀d:cat-ob(D)
     ((cat-comp(C) (F d) (F (G (F d))) (F d) (F d (G (F d)) (eta d)) (eps (F d)))
     = (cat-id(C) (F d))
     ∈ (cat-arrow(C) (F d) (F d))))
  ∧ (∀c:cat-ob(C)
       ((cat-comp(D) (G c) (G (F (G c))) (G c) (eta (G c)) (G (F (G c)) c (eps c)))
       = (cat-id(D) (G c))
       ∈ (cat-arrow(D) (G c) (G c))))
Lemma: counit-unit-equations_wf
∀[A,B:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;A)]. ∀[eps:b:cat-ob(B) ⟶ (cat-arrow(B) (F (G b)) b)].
∀[eta:a:cat-ob(A) ⟶ (cat-arrow(A) a (G (F a)))].
  (counit-unit-equations(A;B;F;G;eps;eta) ∈ ℙ)
Definition: counit-unit-adjunction
F -| G ==
  {p:nat-trans(B;B;functor-comp(G;F);1) × nat-trans(A;A;1;functor-comp(F;G))| 
   counit-unit-equations(A;B;F;G;fst(p);snd(p))} 
Lemma: counit-unit-adjunction_wf
∀[A,B:SmallCategory].  ∀F:Functor(A;B). ∀G:Functor(B;A).  (F -| G ∈ Type)
Definition: mk-adjunction
mk-adjunction(b.eps[b];a.eta[a]) ==  <b |→ eps[b], a |→ eta[a]>
Lemma: mk-adjunction_wf
∀[A,B:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;A)]. ∀[eps:b:cat-ob(B) ⟶ (cat-arrow(B) (F (G b)) b)].
∀[eta:a:cat-ob(A) ⟶ (cat-arrow(A) a (G (F a)))].
  (mk-adjunction(b.eps[b];a.eta[a]) ∈ F -| G) supposing 
     ((∀a1,a2:cat-ob(A). ∀g:cat-arrow(A) a1 a2.
         ((cat-comp(A) a1 (G (F a1)) (G (F a2)) eta[a1] (G (F a1) (F a2) (F a1 a2 g)))
         = (cat-comp(A) a1 a2 (G (F a2)) g eta[a2])
         ∈ (cat-arrow(A) a1 (G (F a2))))) and 
     (∀b1,b2:cat-ob(B). ∀g:cat-arrow(B) b1 b2.
        ((cat-comp(B) (F (G b1)) b1 b2 eps[b1] g)
        = (cat-comp(B) (F (G b1)) (F (G b2)) b2 (F (G b1) (G b2) (G b1 b2 g)) eps[b2])
        ∈ (cat-arrow(B) (F (G b1)) b2))) and 
     counit-unit-equations(A;B;F;G;λb.eps[b];λa.eta[a]))
Lemma: free-group-adjunction
FreeGp -| ForgetGroup
Lemma: free-dist-lattice-adjunction
FreeDistLattice -| ForgetLattice
Definition: cat-monad
Monad(C) ==
  {M:T:Functor(C;C) × nat-trans(C;C;1;T) × nat-trans(C;C;functor-comp(T;T);T)| 
   let T,u,m = M in 
   (∀X:cat-ob(C)
      ((cat-comp(C) (T X) (T (T X)) (T X) (u (T X)) (m X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
   ∧ (∀X:cat-ob(C)
        ((cat-comp(C) (T X) (T (T X)) (T X) (T X (T X) (u X)) (m X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
   ∧ (∀X:cat-ob(C)
        ((cat-comp(C) (T (T (T X))) (T (T X)) (T X) (m (T X)) (m X))
        = (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (T X) (m X)) (m X))
        ∈ (cat-arrow(C) (T (T (T X))) (T X))))} 
Lemma: cat-monad_wf
∀[C:SmallCategory]. (Monad(C) ∈ Type)
Definition: mk-monad
mk-monad(T;u;m) ==  <T, u, m>
Lemma: mk-monad_wf
∀[C:SmallCategory]. ∀[T:Functor(C;C)]. ∀[u:nat-trans(C;C;1;T)]. ∀[m:nat-trans(C;C;functor-comp(T;T);T)].
  (mk-monad(T;
            u;
            m) ∈ Monad(C)) supposing 
     ((∀X:cat-ob(C)
         ((cat-comp(C) (T X) (T (T X)) (T X) (u (T X)) (m X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X)))) and 
     (∀X:cat-ob(C)
        ((cat-comp(C) (T X) (T (T X)) (T X) (T X (T X) (u X)) (m X))
        = (cat-id(C) (T X))
        ∈ (cat-arrow(C) (T X) (T X)))) and 
     (∀X:cat-ob(C)
        ((cat-comp(C) (T (T (T X))) (T (T X)) (T X) (m (T X)) (m X))
        = (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (T X) (m X)) (m X))
        ∈ (cat-arrow(C) (T (T (T X))) (T X)))))
Definition: monad-functor
monad-functor(M) ==  fst(M)
Lemma: monad-functor_wf
∀[C:SmallCategory]. ∀[M:Monad(C)].  (monad-functor(M) ∈ Functor(C;C))
Definition: monad-fun
M(x) ==  monad-functor(M) x
Lemma: monad-fun_wf
∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x:cat-ob(C)].  (M(x) ∈ cat-ob(C))
Definition: monad-unit
monad-unit(M;x) ==  (fst(snd(M))) x
Lemma: monad-unit_wf
∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x:cat-ob(C)].  (monad-unit(M;x) ∈ cat-arrow(C) x M(x))
Definition: monad-op
monad-op(M;x) ==  (snd(snd(M))) x
Lemma: monad-op_wf
∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x:cat-ob(C)].  (monad-op(M;x) ∈ cat-arrow(C) M(M(x)) M(x))
Lemma: monad-equations
∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x:cat-ob(C)].
  ((((cat-comp(C) M(x) M(M(x)) M(x) monad-unit(M;M(x)) monad-op(M;x)) = (cat-id(C) M(x)) ∈ (cat-arrow(C) M(x) M(x)))
  ∧ ((cat-comp(C) M(x) M(M(x)) M(x) (monad-functor(M) x M(x) monad-unit(M;x)) monad-op(M;x))
    = (cat-id(C) M(x))
    ∈ (cat-arrow(C) M(x) M(x))))
  ∧ ((cat-comp(C) M(M(M(x))) M(M(x)) M(x) monad-op(M;M(x)) monad-op(M;x))
    = (cat-comp(C) M(M(M(x))) M(M(x)) M(x) (monad-functor(M) M(M(x)) M(x) monad-op(M;x)) monad-op(M;x))
    ∈ (cat-arrow(C) M(M(M(x))) M(x))))
Definition: monad-extend
monad-extend(C;M;x;y;f) ==  cat-comp(C) M(x) M(M(y)) M(y) (monad-functor(M) x M(y) f) monad-op(M;y)
Lemma: monad-extend_wf
∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x M(y)].
  (monad-extend(C;M;x;y;f) ∈ cat-arrow(C) M(x) M(y))
Lemma: monad-unit-extend
∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x M(y)].
  ((cat-comp(C) x M(x) M(y) monad-unit(M;x) monad-extend(C;M;x;y;f)) = f ∈ (cat-arrow(C) x M(y)))
Lemma: monad-extend-unit
∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[y:cat-ob(C)].
  (monad-extend(C;M;y;y;monad-unit(M;y)) = (cat-id(C) M(y)) ∈ (cat-arrow(C) M(y) M(y)))
Lemma: monad-extend-comp
∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x,y,z:cat-ob(C)]. ∀[g:cat-arrow(C) x M(y)]. ∀[h:cat-arrow(C) y M(z)].
  (monad-extend(C;M;x;z;cat-comp(C) x M(y) M(z) g monad-extend(C;M;y;z;h))
  = (cat-comp(C) M(x) M(y) M(z) monad-extend(C;M;x;y;g) monad-extend(C;M;y;z;h))
  ∈ (cat-arrow(C) M(x) M(z)))
Lemma: equal-monads
∀[C:SmallCategory]. ∀[M1,M2:Monad(C)].
  (M1 = M2 ∈ Monad(C)) supposing 
     ((∀x:cat-ob(C). (monad-op(M1;x) = monad-op(M2;x) ∈ (cat-arrow(C) M1(M1(x)) M1(x)))) and 
     (∀x:cat-ob(C). (monad-unit(M1;x) = monad-unit(M2;x) ∈ (cat-arrow(C) x M1(x)))) and 
     (monad-functor(M1) = monad-functor(M2) ∈ Functor(C;C)))
Definition: adjunction-monad
adjMonad(adj) ==  mk-monad(functor-comp(F;G);snd(adj);x |→ G (F (G (F x))) (F x) ((fst(adj)) (F x)))
Lemma: adjunction-monad_wf
∀[A,B:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;A)]. ∀[adj:F -| G].  (adjMonad(adj) ∈ Monad(A))
Definition: Kleisli-cat
Kl(C;M) ==
  Cat(ob = cat-ob(C);
      arrow(x,y) = cat-arrow(C) x M(y);
      id(x) = monad-unit(M;x);
      comp(x,y,z,f,g) = cat-comp(C) x M(y) M(z) f monad-extend(C;M;y;z;g))
Lemma: Kleisli-cat_wf
∀[C:SmallCategory]. ∀M:Monad(C). (Kl(C;M) ∈ SmallCategory)
Definition: Kleisli-left
KlF(C;M) ==  functor(ob(x) = x;arrow(x,y,f) = monad-unit(M;y) o f)
Lemma: Kleisli-left_wf
∀[C:SmallCategory]. ∀M:Monad(C). (KlF(C;M) ∈ Functor(C;Kl(C;M)))
Definition: Kleisli-right
KlG(C;M) ==  functor(ob(y) = M(y);arrow(x,y,f) = monad-extend(C;M;x;y;f))
Lemma: Kleisli-right_wf
∀[C:SmallCategory]. ∀M:Monad(C). (KlG(C;M) ∈ Functor(Kl(C;M);C))
Definition: Kleisli-adjunction
Kl(C;M) ==  mk-adjunction(y.cat-id(C) M(y);x.monad-unit(M;x))
Lemma: Kleisli-adjunction_wf
∀[C:SmallCategory]. ∀[M:Monad(C)].  (Kl(C;M) ∈ KlF(C;M) -| KlG(C;M))
Lemma: monad-of-Kleisli-adjunction
∀[C:SmallCategory]. ∀[M:Monad(C)].  (adjMonad(Kl(C;M)) = M ∈ Monad(C))
Definition: monad-from
monad-from(Mnd) ==
  mk-monad(functor(ob(T) = M-map(Mnd) T;
                   arrow(X,Y,f) = λz.(M-bind(Mnd) z (λx.(M-return(Mnd) (f x)))));
           λx.M-return(Mnd);
           λx,z. (M-bind(Mnd) z (λx.x)))
Lemma: monad-from_wf
∀[Mnd:Monad]. (monad-from(Mnd) ∈ Monad(TypeCat))
Definition: bag-cat-monad
bag-cat-monad() ==  mk-monad(functor(ob(x) = bag(x);arrow(x,y,f) = λz.bag-map(f;z));x |→ λz.{z};x |→ λz.bag-union(z))
Lemma: bag-cat-monad_wf
bag-cat-monad() ∈ Monad(TypeCat)
Home
Index