---

Step * of Lemma csm-cubical-type-ap-morph

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I,J,f,a,u,s:Top].  ((u a f) ~ (u (s)a f))
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 2 (DVar `A')
   THEN RepUR ``cubical-type-ap-morph csm-ap-type cubical-type-at csm-ap`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[I,J,f,a,u,s:Top].    ((u  a  f)  \msim{}  (u  (s)a  f))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  (DVar  `A')
  THEN  RepUR  ``cubical-type-ap-morph  csm-ap-type  cubical-type-at  csm-ap``  0
  THEN  Auto)

---

Home Index