---

Step * of Lemma forget-group_wf

ForgetGroup ∈ Functor(Group;TypeCat)
BY
{ (Unfold `forget-group` 0 THEN MemCD THEN Try (QuickAuto) THEN All (RepUR  ``type-cat group-cat mk-cat``) THEN Auto) }

---

Latex:

---

Latex:
ForgetGroup  \mmember{}  Functor(Group;TypeCat)


By

---

Latex:
(Unfold  `forget-group`  0
  THEN  MemCD
  THEN  Try  (QuickAuto)
  THEN  All  (RepUR    ``type-cat  group-cat  mk-cat``)
  THEN  Auto)

---

Home Index