---

Step * of Lemma counit-unit-equations_wf

No Annotations
∀[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) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:SmallCategory].  \mforall{}[F:Functor(A;B)].  \mforall{}[G:Functor(B;A)].  \mforall{}[eps:b:cat-ob(B)  {}\mrightarrow{}  (cat-arrow(B) 
                                                                                                                                                                    (F  (G  b)) 
                                                                                                                                                                    b)].
\mforall{}[eta:a:cat-ob(A)  {}\mrightarrow{}  (cat-arrow(A)  a  (G  (F  a)))].
    (counit-unit-equations(A;B;F;G;eps;eta)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index