---

Step * of Lemma csm-id-comp

∀[A,B:CubicalSet]. ∀[sigma:A ⟶ B].  ((sigma o 1(A) = sigma ∈ A ⟶ B) ∧ (1(B) o sigma = sigma ∈ A ⟶ B))
BY
{ (Auto
   THEN Unfolds ``cube-set-map csm-comp csm-id`` 0
   THEN InstLemma `cubical-set-is-functor` []
   THEN D -1
   THEN RWW "trans-id-property.0" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:CubicalSet].  \mforall{}[sigma:A  {}\mrightarrow{}  B].    ((sigma  o  1(A)  =  sigma)  \mwedge{}  (1(B)  o  sigma  =  sigma))


By

---

Latex:
(Auto
  THEN  Unfolds  ``cube-set-map  csm-comp  csm-id``  0
  THEN  InstLemma  `cubical-set-is-functor`  []
  THEN  D  -1
  THEN  RWW  "trans-id-property.0"  0
  THEN  Auto)

---

Home Index