Lemma: pi1_wf_top
[T:Type]. ∀[p:T × Top].  (fst(p) ∈ T)

Definition: small-category
SmallCategory ==
   × arrow:ob ⟶ ob ⟶ Type
   × x:ob ⟶ (arrow x)
   × (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow y) ⟶ (arrow z) ⟶ (arrow z))| 
   let ob,arrow,id,comp cat 
   in (∀x,y:ob. ∀f:arrow y.  (((comp (id x) f) f ∈ (arrow y)) ∧ ((comp (id y)) f ∈ (arrow y))))
      ∧ (∀x,y,z,w:ob. ∀f:arrow y. ∀g:arrow z. ∀h:arrow w.
           ((comp (comp g) h) (comp (comp h)) ∈ (arrow w)))  

Lemma: small-category_wf
SmallCategory ∈ 𝕌'

Lemma: small-category-subtype
SmallCategory ⊆SmallCategory'

Lemma: small-category-subtype'
SmallCategory ⊆small-category{i'':l}

Lemma: small-category-cumulativity-2
SmallCategory ⊆small-category{[j 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))

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
  (cat-comp(C) ∈ x:cat-ob(C)
   ⟶ y:cat-ob(C)
   ⟶ z:cat-ob(C)
   ⟶ (cat-arrow(C) y)
   ⟶ (cat-arrow(C) z)
   ⟶ (cat-arrow(C) z))

Lemma: cat_comp_tuple_lemma
y,x,arrow,ob:Top.  (cat-comp(<ob, arrow, x, y>y)

Definition: cat_comp
==  cat-comp(C) g

Lemma: cat_comp_wf
[C:SmallCategory]. ∀[x,y,z:cat-ob(C)]. ∀[f:cat-arrow(C) y]. ∀[g:cat-arrow(C) z].  (g f ∈ cat-arrow(C) 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;
                           g]) ==
  , λx,y. arrow[x; y]
  , λa.id[a]
  , λu,v,w,f,g. comp[u;

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) y ∈ X;id(a) = ⋅;comp(u,v,w,f,g) = ⋅)

Lemma: discrete-cat_wf
[X:Type]. (discrete-cat(X) ∈ SmallCategory)

Definition: unit-cat
==  discrete-cat(Unit)

Lemma: unit-cat_wf
1 ∈ SmallCategory

Definition: cat-inverse
fg=1 ==  (cat-comp(C) g) (cat-id(C) x) ∈ (cat-arrow(C) x)

Lemma: cat-inverse_wf
[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) y]. ∀[g:cat-arrow(C) x].  (fg=1 ∈ ℙ)

Definition: cat-co-retraction
co-retraction(f) ==  ∃g:cat-arrow(C) x. fg=1

Lemma: cat-co-retraction_wf
[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) y].  (co-retraction(f) ∈ ℙ)

Definition: cat-retraction
retraction(g) ==  ∃f:cat-arrow(C) y. fg=1

Lemma: cat-retraction_wf
[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[g:cat-arrow(C) x].  (retraction(g) ∈ ℙ)

Lemma: cat-comp-assoc
  ∀x,y,z,w:cat-ob(C). ∀f:cat-arrow(C) y. ∀g:cat-arrow(C) z. ∀h:cat-arrow(C) w.
    ((cat-comp(C) (cat-comp(C) g) h) (cat-comp(C) (cat-comp(C) h)) ∈ (cat-arrow(C) w))

Lemma: cat_comp_assoc
  ∀x,y,z,w:cat-ob(C). ∀f:cat-arrow(C) y. ∀g:cat-arrow(C) z. ∀h:cat-arrow(C) w.
    (h f ∈ (cat-arrow(C) w))

Lemma: cat-comp-ident
  ∀x,y:cat-ob(C). ∀f:cat-arrow(C) y.
    (((cat-comp(C) (cat-id(C) x) f) f ∈ (cat-arrow(C) y))
    ∧ ((cat-comp(C) (cat-id(C) y)) f ∈ (cat-arrow(C) y)))

Lemma: cat-comp-ident1
[C:SmallCategory]. ∀x,y:cat-ob(C). ∀f:cat-arrow(C) y.  ((cat-comp(C) (cat-id(C) x) f) f ∈ (cat-arrow(C) y))

Lemma: cat-comp-ident2
[C:SmallCategory]. ∀x,y:cat-ob(C). ∀f:cat-arrow(C) y.  ((cat-comp(C) (cat-id(C) y)) f ∈ (cat-arrow(C) y))

Lemma: left-right-inverse-unique
[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) y]. ∀[g2:cat-arrow(C) x].
  ∀[g1:cat-arrow(C) x]. g1 g2 ∈ (cat-arrow(C) x) supposing fg1=1 supposing g2f=1

Definition: cat-isomorphism
cat-isomorphism(C;x;y;f) ==  ∃g:cat-arrow(C) x. (fg=1 ∧ gf=1)

Lemma: cat-isomorphism_wf
[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) y].  (cat-isomorphism(C;x;y;f) ∈ ℙ)

Lemma: cat-inverse-unique
[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) y]. ∀[g2,g1:cat-arrow(C) x].
  (g1 g2 ∈ (cat-arrow(C) x)) supposing ((∃h:cat-arrow(C) 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) b. ∀g:cat-arrow(C) c.
  (cat-isomorphism(C;a;b;f)  cat-isomorphism(C;b;c;g)  cat-isomorphism(C;a;c;cat-comp(C) g))

Definition: cat-isomorphic
cat-isomorphic(C;x;y) ==  ∃f:cat-arrow(C) 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 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) y].
    h ∈ (cat-arrow(C) y) supposing (cat-comp(C) f) (cat-comp(C) f) ∈ (cat-arrow(C) z)

Lemma: cat-monic_wf
[C:SmallCategory]. ∀[y,z:cat-ob(C)]. ∀[f:cat-arrow(C) z].  (monic(f) ∈ ℙ)

Lemma: co-retraction-monic
[C:SmallCategory]. ∀[y,z:cat-ob(C)]. ∀[f:cat-arrow(C) z].  monic(f) supposing co-retraction(f)

Definition: cat-epic
epic(f) ==
  ∀[z:cat-ob(C)]. ∀[g,h:cat-arrow(C) z].
    h ∈ (cat-arrow(C) z) supposing (cat-comp(C) g) (cat-comp(C) h) ∈ (cat-arrow(C) z)

Lemma: cat-epic_wf
[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) y].  (epic(f) ∈ ℙ)

Lemma: retraction-epic
[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) y].  epic(f) supposing retraction(f)

Definition: cat-initial
Initial(i) ==  ∀[x:cat-ob(C)]. ((∀[f,g:cat-arrow(C) x].  (f g ∈ (cat-arrow(C) x))) ∧ (cat-arrow(C) 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) fnl].  (f g ∈ (cat-arrow(C) fnl))) ∧ (cat-arrow(C) 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) y) ⟶ (cat-arrow(C2) (F x) (F y)))| 
   let F,M FM 
   in (∀x:cat-ob(C1). ((M (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) y. ∀g:cat-arrow(C1) z.
           ((M (cat-comp(C1) g))
           (cat-comp(C2) (F x) (F y) (F z) (M f) (M 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;
                             f]) ==
  , λx,y,f. arrow[x;

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) 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) y. ∀g:cat-arrow(A) z.
        (M[x;z;cat-comp(A) 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]) 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) 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]) arrow[x;y;g])

Lemma: arrow_pair_lemma
y,x:Top.  (arrow(<x, y>y)

Definition: functor_arrow
F(f) ==  f

Lemma: functor_arrow_wf
[C,D:SmallCategory]. ∀[F:Functor(C;D)]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) 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 (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) y]. ∀[g:cat-arrow(C) z].
  ((F (cat-comp(C) g)) (cat-comp(D) (F x) (F y) (F z) (F f) (F 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) y;cat-arrow(D) (F x) (F y);F 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) B.
     ((cat-comp(D) (F A) (G A) (G B) (trans A) (G g))
     (cat-comp(D) (F A) (F B) (G B) (F 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) B.
              ((cat-comp(D) (F A) (G A) (G B) (trans A) (G g))
              (cat-comp(D) (F A) (F B) (G B) (F 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) B].
  ((cat-comp(D) (F A) (G A) (G B) (T A) (G g))
  (cat-comp(D) (F A) (F B) (G B) (F 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) B].
[h:cat-arrow(C) B'].
  ((cat-comp(D) (F A) (G B) (G B') (cat-comp(D) (F A) (F B) (G B) (F g) (T B)) (G B' h))
  (cat-comp(D) (F A) (F B') (G B') (cat-comp(D) (F A) (F B) (F B') (F g) (F 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) B]. ∀[v:cat-ob(E)].
  ((cat-comp(E) (J (F A)) (J (G B)) 
    (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 g))))
  (cat-comp(E) (J (F A)) (J (G B)) 
     (cat-comp(E) (J (F A)) (J (F B)) (J (G B)) (J (F A) (F B) (F 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))].
  B ∈ nat-trans(C;D;F;G) supposing 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)].
  B ∈ nat-trans(C;D;F;G) supposing B ∈ (A:cat-ob(C) ⟶ (cat-arrow(D) (F A) (G A)))

Definition: mk-nat-trans
|→ 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))].
  |→ trans[x] ∈ nat-trans(C;D;F;G) 
  supposing ∀A,B:cat-ob(C). ∀g:cat-arrow(C) B.
              ((cat-comp(D) (F A) (G A) (G B) trans[A] (G g))
              (cat-comp(D) (F A) (F B) (G B) (F g) trans[B])
              ∈ (cat-arrow(D) (F A) (G B)))

Lemma: ap_mk_nat_trans_lemma
z,T:Top.  (b |→ T[b] T[z])

Definition: identity-trans
identity-trans(C;D;F) ==  |→ 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) cat-id(D) (F A))

Definition: trans-comp
t1 t2 ==  |→ 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 t2 ∈ nat-trans(C;D;F;H))

Lemma: trans_comp_ap_lemma
A,t2,t1,H,G,F,D,C:Top.  (t1 t2 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) f ∈ nat-trans(C1;C2;x;y)) ∧ (f 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).
  (f 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) B].
  ((cat-comp(D) (F A) (H A) (H B) (cat-comp(D) (F A) (G A) (H A) (t1 A) (t2 A)) (H g))
  (cat-comp(D) (F A) (F B) (H B) (F 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) B]. ∀[h:cat-arrow(C) B'].
  ((cat-comp(D) (F A) (G B) (G B') 
    (cat-comp(D) (F A) (F B) (G B) (F g) (cat-comp(D) (F B) (H B) (G B) (t1 B) (t2 B))) 
    (G B' h))
  (cat-comp(D) (F A) (F B') (G B') (cat-comp(D) (F A) (F B) (F B') (F g) (F 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 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)) nat-trans(A;B;F;G))

Lemma: functor_cat_id_lemma
F,B,A:Top.  (cat-id(FUN(A;B)) identity-trans(A;B;F))

Lemma: functor_cat_comp_lemma
t2,t1,H,G,F,B,A:Top.  (cat-comp(FUN(A;B)) t1 t2 t1 t2)

Definition: op-cat
op-cat(C) ==  let ob,arrow,id,comp in <ob, λx,y. (arrow x), id, λx,y,z,f,g. (comp 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)) cat-arrow(C) A)

Lemma: op-cat-comp
C:SmallCategory. ∀[I,J,K,f,g:Top].  (cat-comp(op-cat(C)) cat-comp(C) f)

Lemma: op-cat-id
C:SmallCategory. ∀[A:Top]. (cat-id(op-cat(C)) cat-id(C) A)

Definition: op-functor
op-functor(F) ==  functor(ob(x) x;arrow(a,b,f) 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 f)>

Lemma: type-cat_wf
TypeCat ∈ SmallCategory'

Lemma: void-initial-type

Lemma: top-final-type

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_wf1
[C:SmallCategory]. (presheaf{j:l}(C) ∈ 𝕌{[i j']})

Lemma: presheaf_wf
[C:SmallCategory]. (Presheaf(C) ∈ 𝕌')

Lemma: presheaf-cumulativity1
[C:SmallCategory]. (presheaf{j:l}(C) ⊆presheaf{[i j]:l}(C))

Definition: ext-equal-presheaves
ext-equal-presheaves(C;F;G) ==
  (∀x:cat-ob(C). x ≡ x) ∧ (∀x,y:cat-ob(C). ∀f:cat-arrow(C) x.  ((F f) (G 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;
                                     rho]) ==
  functor(ob(I) S[I];
          arrow(I,J,f) = λrho.morph[I;

Lemma: mk-presheaf_wf1
[C:SmallCategory]. ∀[S:cat-ob(C) ⟶ 𝕌{j}]. ∀[morph:I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) I) ⟶ S[I] ⟶ S[J]].
  (Presheaf(Set(I) =S[I];
            Morphism(I,J,f,rho) morph[I;J;f;rho]) ∈ presheaf{j:l}(C)) supposing 
     ((∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) I. ∀g:cat-arrow(C) J. ∀rho:S[I].
         (morph[I;K;cat-comp(C) 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])))

Lemma: mk-presheaf_wf
[C:SmallCategory]. ∀[S:cat-ob(C) ⟶ Type]. ∀[morph:I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) 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) I. ∀g:cat-arrow(C) J. ∀rho:S[I].
         (morph[I;K;cat-comp(C) 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) X), λU,U',f,ux. (cat-comp(C) U' 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) X| f} , λU,U',f,ux. (cat-comp(C) U' ux)>

Lemma: rep-sub-sheaf_wf
[C:SmallCategory]. ∀[X:cat-ob(C)]. ∀[P:U:cat-ob(C) ⟶ (cat-arrow(C) X) ⟶ ℙ].
  rep-sub-sheaf(C;X;P) ∈ Functor(op-cat(C);TypeCat) 
  supposing ∀A,B:cat-ob(C). ∀g:cat-arrow(C) B. ∀b:{b:cat-arrow(C) X| b} .  (P (cat-comp(C) b))

Definition: yoneda-embedding
yoneda-embedding(C) ==  functor(ob(X) rep-pre-sheaf(C;X);arrow(X,Y,f) |→ λg.(cat-comp(C) 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) (F x);arrow(x,y,a) (F x) (F y) (F 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) y)
                                                                        ⟶ (cat-arrow(B) (F x) (F y)))].
  (F G ∈ Functor(A;B)) supposing 
     ((∀x,y:cat-ob(A). ∀f:cat-arrow(A) y.  ((F f) ((snd(G)) 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) y.  ((F f) (G 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)].
  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)) y.  ((F f) (G 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
==  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
    ⇐⇒ Bij(cat-ob(A);cat-ob(B);ob(f)) ∧ (∀x,y:cat-ob(A).  Bij(cat-arrow(A) y;cat-arrow(B) (f x) (f y);f y)))

Definition: product-cat
A × ==
  <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) 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) ~ <cat-id(A) (fst(x)), cat-id(B) (snd(x))>)

Lemma: comp_product_cat_lemma
  (cat-comp(A × B) ~ <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 g, cat-comp(B) b1 b2 b3 k>)
  ∈ (cat-arrow(C) (F <a1, b1>(F <a3, b3>)))

Definition: trans-horizontal-comp
trans-horizontal-comp(E;F;G;J;K;tFG;tJK) ==
  |→ 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) trans-horizontal-comp(E;G;H;J;K;tGH;tJK)
  trans-horizontal-comp(E;F;H;I;K;tFG tGH;tIJ 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) |→ F <x, b> <y, b> <f, cat-id(B) b>);
          arrow(F,G,T) |→ |→ 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) (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 |→ (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 y1_z x_y2 y2_z ==  (cat-comp(C) y1 x_y1 y1_z) (cat-comp(C) y2 x_y2 y2_z) ∈ (cat-arrow(C) z)

Lemma: cat-square-commutes_wf
[C:SmallCategory]. ∀[x,y1,y2,z:cat-ob(C)]. ∀[x_y1:cat-arrow(C) y1]. ∀[y1_z:cat-arrow(C) y1 z]. ∀[x_y2:cat-arrow(C) 
[y2_z:cat-arrow(C) y2 z].
  (x_y1 y1_z x_y2 y2_z ∈ ℙ)

Lemma: cat-square-commutes-sym
[C:SmallCategory]. ∀[x,y1,y2,z:cat-ob(C)]. ∀[x_y1:cat-arrow(C) y1]. ∀[y1_z:cat-arrow(C) y1 z]. ∀[x_y2:cat-arrow(C) 
[y2_z:cat-arrow(C) y2 z].
  uiff(x_y1 y1_z x_y2 y2_z;x_y2 y2_z x_y1 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 cat-comp(C) y1 y2 y3 y1_y2 y2_y3 cat-comp(C) x1 x2 x3 x1_x2 x2_x3 x3_y3) supposing 
     (x1_y1 y1_y2 x1_x2 x2_y2 and 
     x2_y2 y2_y3 x2_x3 x3_y3)

Definition: groupoid
Groupoid ==
  C:SmallCategory × {inv:x:cat-ob(C) ⟶ y:cat-ob(C) ⟶ (cat-arrow(C) y) ⟶ (cat-arrow(C) x)| 
                     ∀x,y:cat-ob(C). ∀f:cat-arrow(C) y.
                       (((cat-comp(C) (inv f)) (cat-id(C) x) ∈ (cat-arrow(C) x))
                       ∧ ((cat-comp(C) (inv f) f) (cat-id(C) y) ∈ (cat-arrow(C) 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

Lemma: groupoid-inv_wf
[G:Groupoid]. ∀[x,y:cat-ob(cat(G))]. ∀[x_y:cat-arrow(cat(G)) y].  (groupoid-inv(G;x;y;x_y) ∈ cat-arrow(cat(G)) x)

Lemma: groupoid_inv
  ∀x,y:cat-ob(cat(G)). ∀f:cat-arrow(cat(G)) y.
    (((cat-comp(cat(G)) groupoid-inv(G;x;y;f)) (cat-id(cat(G)) x) ∈ (cat-arrow(cat(G)) x))
    ∧ ((cat-comp(cat(G)) groupoid-inv(G;x;y;f) f) (cat-id(cat(G)) y) ∈ (cat-arrow(cat(G)) y)))

Definition: mk-groupoid
         inv(x,y,f) inv[x;
                          f]) ==
  , λx,y,f. inv[x;

Lemma: mk-groupoid_wf
[C:SmallCategory]. ∀[inv:x:cat-ob(C) ⟶ y:cat-ob(C) ⟶ (cat-arrow(C) y) ⟶ (cat-arrow(C) x)].
           inv(x,y,f) inv[x;y;f]) ∈ Groupoid 
  supposing ∀x,y:cat-ob(C). ∀f:cat-arrow(C) y.
              (((cat-comp(C) inv[x;y;f]) (cat-id(C) x) ∈ (cat-arrow(C) x))
              ∧ ((cat-comp(C) inv[x;y;f] f) (cat-id(C) y) ∈ (cat-arrow(C) y)))

Definition: groupoid-map
groupoid-map(G;H) ==
   ∀x,y:cat-ob(cat(G)). ∀f:cat-arrow(cat(G)) y.
     ((F groupoid-inv(G;x;y;f)) groupoid-inv(H;F x;F y;F 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)) y]. ∀[c:cat-arrow(cat(G)) z].
  uiff((cat-comp(cat(G)) c) (cat-comp(cat(G)) c) ∈ (cat-arrow(cat(G)) z);a
  ∈ (cat-arrow(cat(G)) y))

Lemma: groupoid-left-cancellation
[G:Groupoid]. ∀[x,y,z:cat-ob(cat(G))]. ∀[a,b:cat-arrow(cat(G)) z]. ∀[c:cat-arrow(cat(G)) y].
  uiff((cat-comp(cat(G)) a) (cat-comp(cat(G)) b) ∈ (cat-arrow(cat(G)) z);a
  ∈ (cat-arrow(cat(G)) z))

Lemma: groupoid-square-commutes-iff
[G:Groupoid]. ∀[x,y1,y2,z:cat-ob(cat(G))]. ∀[x_y1:cat-arrow(cat(G)) y1]. ∀[y1_z:cat-arrow(cat(G)) y1 z].
[x_y2:cat-arrow(cat(G)) y2]. ∀[y2_z:cat-arrow(cat(G)) y2 z].
  uiff(x_y1 y1_z x_y2 y2_z;y2_z
  (cat-comp(cat(G)) y2 groupoid-inv(G;x;y2;x_y2) (cat-comp(cat(G)) y1 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)) y1]. ∀[y1_z:cat-arrow(cat(G)) y1 z].
[x_y2:cat-arrow(cat(G)) y2]. ∀[y2_z:cat-arrow(cat(G)) y2 z].
  uiff(x_y1 y1_z x_y2 y2_z;x_y1
  (cat-comp(cat(G)) y1 (cat-comp(cat(G)) y2 x_y2 y2_z) groupoid-inv(G;y1;z;y1_z))
  ∈ (cat-arrow(cat(G)) 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 supposing a ∧ b ∧ k ∧ l ∧ h
  ∧ supposing d ∧ b ∧ k ∧ l ∧ h
  ∧ supposing a ∧ d ∧ k ∧ l ∧ h
  ∧ supposing a ∧ b ∧ d ∧ l ∧ h
  ∧ supposing a ∧ b ∧ k ∧ d ∧ h
  ∧ supposing a ∧ b ∧ k ∧ l ∧ 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 d;e h) supposing a ∧ b ∧ k ∧ 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 d;e h) supposing e ∧ f ∧ h ∧ 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 d;e 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 a ∧ b ∧ k ∧ 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 e ∧ f ∧ h ∧ 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| 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 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| 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 in 
      let a',b',f' in 
      {gh:cat-arrow(A) a' × (cat-arrow(B) b')| 
       (cat-comp(C) (S a) (T b) (T b') (T b' (snd(gh))))
       (cat-comp(C) (S a) (S a') (T b') (S a' (fst(gh))) f')
       ∈ (cat-arrow(C) (S a) (T b'))} ;
      id(x) let a,b,f in 
      <cat-id(A) a, cat-id(B) b>;
      comp(u,v,w,fp,gp) let a,b,x in 
      let a',b',x' in 
      let a'',b'',x'' in 
      let f,g fp 
      in let f',g' gp 
         in <cat-comp(A) a' a'' f', cat-comp(B) b' b'' 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) 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)) A| (P 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)) 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)) A| (P 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)) 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) I. ∀rho:F I.  (P[I; rho]  P[J; rho])

Lemma: stable-element-predicate_wf1
[C:SmallCategory]. ∀[F:presheaf{j:l}(C)]. ∀[P:I:cat-ob(C) ⟶ (F I) ⟶ ℙ{j}].
  (stable-element-predicate(C;F;I,rho.P[I;rho]) ∈ ℙ{[i j]})

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

Lemma: presheaf-subset_wf1
[C:SmallCategory]. ∀[F:presheaf{j:l}(C)]. ∀[P:I:cat-ob(C) ⟶ (F I) ⟶ ℙ{j}].
  F|I,rho.P[I;rho] ∈ presheaf{j:l}(C) supposing stable-element-predicate(C;F;I,rho.P[I;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{j:l}(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 ⟶ ==  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 in <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: counit-unit-equations
counit-unit-equations(D;C;F;G;eps;eta) ==
     ((cat-comp(C) (F d) (F (G (F d))) (F d) (F (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)) (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) (G (F a)))].
  (counit-unit-equations(A;B;F;G;eps;eta) ∈ ℙ)

Definition: counit-unit-adjunction
-| ==
  {p:nat-trans(B;B;functor-comp(G;F);1) × nat-trans(A;A;1;functor-comp(F;G))| 

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]) ==  <|→ eps[b], |→ 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) (G (F a)))].
  (mk-adjunction(b.eps[b];a.eta[a]) ∈ -| 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)) 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 

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 in 
      ((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 (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)].
            m) ∈ Monad(C)) supposing 
         ((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 
        ((cat-comp(C) (T X) (T (T X)) (T X) (T (T X) (u X)) (m X))
        (cat-id(C) (T X))
        ∈ (cat-arrow(C) (T X) (T X)))) and 
        ((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) 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) 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) 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) 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) M(y)].
  ((cat-comp(C) M(x) M(y) monad-unit(M;x) monad-extend(C;M;x;y;f)) f ∈ (cat-arrow(C) 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) M(y)]. ∀[h:cat-arrow(C) M(z)].
  (monad-extend(C;M;x;z;cat-comp(C) M(y) M(z) 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) 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 |→ (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) M(y);
      id(x) monad-unit(M;x);
      comp(x,y,z,f,g) cat-comp(C) M(y) M(z) 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) 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))

Home Index