---

Step * of Lemma identity-functor_wf

Id ∈ Functor
BY
{ (RepUR ``type-functor identity-functor`` 0 THEN MemTypeCD THEN RepUR ``compose`` 0 THEN Auto) }

---

Latex:

---

Latex:
Id  \mmember{}  Functor


By

---

Latex:
(RepUR  ``type-functor  identity-functor``  0  THEN  MemTypeCD  THEN  RepUR  ``compose``  0  THEN  Auto)

---

Home Index