Step
*
of Lemma
csm-interval-type
∀[s:Top]. ((𝕀)s ~ 𝕀)
BY
{ ((Auto THEN RepUR ``interval-type constant-cubical-type csm-ap-type`` 0) THEN Auto) }
Latex:
Latex:
\mforall{}[s:Top].  ((\mBbbI{})s  \msim{}  \mBbbI{})
By
Latex:
((Auto  THEN  RepUR  ``interval-type  constant-cubical-type  csm-ap-type``  0)  THEN  Auto)
Home
Index