Step
*
of Lemma
cu-cube-family-comp
∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[J,L,f,g:Top]. (cu-cube-family(alpha;L;(f o g)) ~ cu-cube-family(f(alpha);L;g))
BY
{ ((UnivCD THENA Auto)
THEN (RWO "cubical-universe-I-cube" 2 THENA Auto)
THEN RepeatFor 4 (D 2)
THEN All Reduce
THEN RepUR ``cu-cube-family cube-set-restriction cubical-universe`` 0⋅
THEN RepUR ``csm-Kan-cubical-type csm-ap-type unit-cube-map csm-ap`` 0
THEN Auto) }
Latex:
Latex:
\mforall{}[I:Cname List]. \mforall{}[alpha:c\mBbbU{}(I)]. \mforall{}[J,L,f,g:Top].
(cu-cube-family(alpha;L;(f o g)) \msim{} cu-cube-family(f(alpha);L;g))
By
Latex:
((UnivCD THENA Auto)
THEN (RWO "cubical-universe-I-cube" 2 THENA Auto)
THEN RepeatFor 4 (D 2)
THEN All Reduce
THEN RepUR ``cu-cube-family cube-set-restriction cubical-universe`` 0\mcdot{}
THEN RepUR ``csm-Kan-cubical-type csm-ap-type unit-cube-map csm-ap`` 0
THEN Auto)
Home
Index