Step
*
of Lemma
cubical-universe-at
No Annotations
∀[I,a:Top]. (c𝕌(a) ~ A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A))
BY
{ ((D 0 THENA Auto)
THEN (RepUR ``cubical-type-at cubical-universe closed-type-to-type`` 0
THEN RepUR ``closed-cubical-universe fibrant-type`` 0
)
THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}[I,a:Top]. (c\mBbbU{}(a) \msim{} A:\{formal-cube(I) \mvdash{} \_\} \mtimes{} formal-cube(I) \mvdash{} CompOp(A))
By
Latex:
((D 0 THENA Auto)
THEN (RepUR ``cubical-type-at cubical-universe closed-type-to-type`` 0
THEN RepUR ``closed-cubical-universe fibrant-type`` 0
)
THEN Auto)
Home
Index