---

Step * of Lemma Kan-groupoid-nerve_wf

∀[G:Groupoid]. (Kan-groupoid-nerve(G) ∈ KanCubicalSet)
BY
{ (Auto THEN MemTypeCD THEN Try (Complete (Auto)) THEN RepUR ``Kan-groupoid-nerve`` 0 THEN Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[G:Groupoid].  (Kan-groupoid-nerve(G)  \mmember{}  KanCubicalSet)


By

---

Latex:
(Auto
  THEN  MemTypeCD
  THEN  Try  (Complete  (Auto))
  THEN  RepUR  ``Kan-groupoid-nerve``  0
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index