---

Step * 2 of Lemma counit-unit-adjunction_wf

.....subterm..... T:t
2:n
1. A : SmallCategory
2. B : SmallCategory
3. F : Functor(A;B)
4. G : Functor(B;A)
5. 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)) ∈ Type
BY
{ (D -1 THEN D -2 THEN D -1 THEN All (RepUR  ``functor-comp id_functor``) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(D  -1  THEN  D  -2  THEN  D  -1  THEN  All  (RepUR    ``functor-comp  id\_functor``)  THEN  Auto)

---

Home Index