---

Step * of Lemma csm-id_wf

∀[X:CubicalSet]. (1(X) ∈ X ⟶ X)
BY
{ (Auto THEN Unfolds ``cube-set-map csm-id`` 0 THEN InstLemma `cubical-set-is-functor` [] THEN D -1 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  (1(X)  \mmember{}  X  {}\mrightarrow{}  X)


By

---

Latex:
(Auto
  THEN  Unfolds  ``cube-set-map  csm-id``  0
  THEN  InstLemma  `cubical-set-is-functor`  []
  THEN  D  -1
  THEN  Auto)

---

Home Index