Lemma: pi1_wf_top
∀[T:Type]. ∀[p:T × Top]. (fst(p) ∈ T)
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}
Lemma: small-category-cumulativity-2
SmallCategory ⊆r 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 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_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) ⊆r presheaf{[i | j]:l}(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_wf1
∀[C:SmallCategory]. ∀[S:cat-ob(C) ⟶ 𝕌{j}]. ∀[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{j:l}(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])))
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_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) = F I J f 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 ⟶ 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: 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]))
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))
Home
Index