---

Step * of Lemma csm-cubical-subset

∀[T,psi,s:Top].  (({t:T | ∀I,alpha. psi[I;alpha;t]})s ~ {t:(T)s | ∀I,alpha. psi[I;(s)alpha;t]})
BY
{ (Intros THEN RepUR ``cubical-subset csm-ap-type`` 0 THEN EqCD THEN RW (SubC (SymbCompC [] 100)) 0 THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T,psi,s:Top].    ((\{t:T  |  \mforall{}I,alpha.  psi[I;alpha;t]\})s  \msim{}  \{t:(T)s  |  \mforall{}I,alpha.  psi[I;(s)alpha;t]\})


By

---

Latex:
(Intros
  THEN  RepUR  ``cubical-subset  csm-ap-type``  0
  THEN  EqCD
  THEN  RW  (SubC  (SymbCompC  []  100))  0
  THEN  Trivial)

---

Home Index