---

Step * of Lemma counit-unit-adjunction_wf

∀[A,B:SmallCategory].  ∀F:Functor(A;B). ∀G:Functor(B;A).  (F -| G ∈ Type)
BY
{ (Intros THEN Unfold `counit-unit-adjunction` 0 THEN MemCD) }

1
.....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

2
.....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

---

Latex:

---

Latex:
\mforall{}[A,B:SmallCategory].    \mforall{}F:Functor(A;B).  \mforall{}G:Functor(B;A).    (F  -|  G  \mmember{}  Type)


By

---

Latex:
(Intros  THEN  Unfold  `counit-unit-adjunction`  0  THEN  MemCD)

---

Home Index