---

Step * 1 of Lemma counit-unit-adjunction_wf

.....subterm..... T:t
1:n
1. A : SmallCategory
2. B : SmallCategory
3. F : Functor(A;B)
4. G : Functor(B;A)
⊢ nat-trans(B;B;functor-comp(G;F);1) × nat-trans(A;A;1;functor-comp(F;G)) ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  SmallCategory
2.  B  :  SmallCategory
3.  F  :  Functor(A;B)
4.  G  :  Functor(B;A)
\mvdash{}  nat-trans(B;B;functor-comp(G;F);1)  \mtimes{}  nat-trans(A;A;1;functor-comp(F;G))  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index