---

Step * of Lemma counit-unit-equations_wf

∀[A,B:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;A)]. ∀[eps:b:cat-ob(B) ⟶ (cat-arrow(B) (ob(F) (ob(G) b)) b)].
∀[eta:a:cat-ob(A) ⟶ (cat-arrow(A) a (ob(G) (ob(F) a)))].
  (counit-unit-equations(A;B;F;G;eps;eta) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index