---

Step * of Lemma ident_trans_ap_lemma

∀A,F,D,C:Top.  (identity-trans(C;D;F) A ~ cat-id(D) (ob(F) A))
BY
{ (RepUR ``identity-trans`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A,F,D,C:Top.    (identity-trans(C;D;F)  A  \msim{}  cat-id(D)  (ob(F)  A))


By

---

Latex:
(RepUR  ``identity-trans``  0  THEN  Auto)

---

Home Index