Step
*
of Lemma
contractible_comp-sq
∀[X,A,cA:Top].
(contractible_comp(X;A;cA)
~ λH,sigma,phi,u,a0.
let a = cA H.𝕀 (λx,x@0. (sigma x (m x x@0))) (λI,rho. phi I (fst(rho)) ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. if (phi I (fst((m I rho)))==1)
then fst((u I (m I rho)))
else fst((a0 I (fst((m I rho)))))
fi )
(λI,a. (fst((a0 I (fst(a)))))) in
let b = let v = λI,a@0. (cA H.((A)sigma)[1(𝕀)].𝕀
(λx,x@0. (sigma x <fst(fst((m x x@0))), ¬(snd((m x x@0)))>))
(λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. if (0==1) then ⋅ else snd(fst((m I rho))) fi )
(λI,a. (snd(fst(a))))
I
<fst(a@0), ¬(snd(a@0))>) in
λI,a@0,J,f,u@0,J@0,f@0,u@1.
(cA H.((A)sigma)[1(𝕀)].𝕀
(λx,x@0. (sigma x <fst(fst(fst(x@0))), snd(x@0)>))
(λI,rho.
phi I (fst(fst(rho))) ∨ dM-to-FL(I;¬(...)) ∨ ...)\000C
(λI,rho. if (phi I (fst(fst(fst(rho))))==1)
then (snd((u I <fst(fst(fst(rho))), snd(rho)>)\000C))
I
1
(v I <fst(fst(rho)), snd(rho)>)
I
1
(snd(fst(rho)))
if (dM-to-FL(I;¬(snd(fst(rho))))==1)
then a I <fst(fst(fst(rho))), snd(rho)>
else v I <fst(fst(rho)), snd(rho)>
fi )
(λI,a. ((snd((a0 I (fst(fst(a)))))) I 1 (v I <fst(a), 0>)\000C I
1
(snd(a))))
J@0
<f@0((f(a@0);u@0)), u@1>) in
cubical-pair(λI,a@0. (a I <a@0, 1(𝕀) I a@0>);b))
BY
{ ((UnivCD THENA Auto)
THEN SqEqualTopToBase
THEN Unfold `contractible_comp` 0
THEN RepUR ``path_comp path_term path-term comp-term comp_term`` 0
THEN ...
THEN RepUR ``case-term case-term cc-fst cc-snd cubical-term-at csm+ csm-comp compose csm-adjoin face-zero csm-ap`` 0
THEN RepUR ``csm-comp-structure csm-comp compose face-or cubical-term-at face-one`` 0) }
1
1. cA : Base
2. A : Base
3. X : Base
⊢ sigma_comp(cA;
pi_comp(X.A;(A)λI,p. (fst(p));λH,sigma,phi,u,a0. (cA H (λx,x@0. (fst((sigma x x@0)))) phi u a0);
λH,sigma,phi,u,a0,I,a,J,f,u@0.
(cA H.𝕀
(λx,x@0. (fst(fst((sigma x
<fst(fst((1(H.𝕀.𝕀) x x@0)))
, snd((1(H.𝕀.𝕀) x x@0))
>)))))
(λI,rho. phi I
(fst(rho)) ∨ dM-to-FL(I;¬(snd(rho))) ∨ dM-to-FL(I;snd(rho))\000C)
(λI,rho. if (phi I (fst(fst(rho)))==1)
then u I <fst(fst(rho)), snd(rho)> I 1 (snd(fst(rho)))
if (dM-to-FL(I;¬(snd(fst(rho))))==1)
then snd(fst((sigma I <fst(fst(rho)), snd(rho)>)))
else snd((sigma I <fst(fst(rho)), snd(rho)>))
fi )
(λI,a. (a0 I (fst(a)) I 1 (snd(a))))
J
<f(a), u@0>)))
~ λH,sigma,phi,u,a0.
let a = cA H.𝕀 (λx,x@0. (sigma x (m x x@0))) (λI,rho. phi I (fst(rho)) ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. if (phi I (fst((m I rho)))==1)
then fst((u I (m I rho)))
else fst((a0 I (fst((m I rho)))))
fi )
(λI,a. (fst((a0 I (fst(a)))))) in
let b = let v = λI,a@0. (cA H.((A)sigma)[1(𝕀)].𝕀
(λx,x@0. (sigma x <fst(fst((m x x@0))), ¬(snd((m x x@0)))>))
(λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. if (0==1) then ⋅ else snd(fst((m I rho))) fi )
(λI,a. (snd(fst(a))))
I
<fst(a@0), ¬(snd(a@0))>) in
λI,a@0,J,f,u@0,J@0,f@0,u@1.
(cA H.((A)sigma)[1(𝕀)].𝕀
(λx,x@0. (sigma x <fst(fst(fst(x@0))), snd(x@0)>))
(λI,rho.
phi I (fst(fst(rho))) ∨ dM-to-FL(I;¬(...)) ∨ ...)
(λI,rho. if (phi I (fst(fst(fst(rho))))==1)
then (snd((u I <fst(fst(fst(rho))), snd(rho)>)))\000C I
1
(v I <fst(fst(rho)), snd(rho)>)
I
1
(snd(fst(rho)))
if (dM-to-FL(I;¬(snd(fst(rho))))==1)
then a I <fst(fst(fst(rho))), snd(rho)>
else v I <fst(fst(rho)), snd(rho)>
fi )
(λI,a. ((snd((a0 I (fst(fst(a)))))) I 1 (v I <fst(a), 0>) I\000C 1
(snd(a))))
J@0
<f@0(<f(a@0), u@0>), u@1>) in
cubical-pair(λI,a@0. (a I <a@0, 1(𝕀) I a@0>);b)
Latex:
Latex:
\mforall{}[X,A,cA:Top].
(contractible\_comp(X;A;cA)
\msim{} \mlambda{}H,sigma,phi,u,a0.
let a = cA H.\mBbbI{} (\mlambda{}x,x@0. (sigma x (m x x@0)))
(\mlambda{}I,rho. phi I (fst(rho)) \mvee{} dM-to-FL(I;\mneg{}(snd(rho))))
(\mlambda{}I,rho. if (phi I (fst((m I rho)))==1)
then fst((u I (m I rho)))
else fst((a0 I (fst((m I rho)))))
fi )
(\mlambda{}I,a. (fst((a0 I (fst(a)))))) in
let b = let v = \mlambda{}I,a@0. (cA H.((A)sigma)[1(\mBbbI{})].\mBbbI{}
(\mlambda{}x,x@0. (sigma x
<fst(fst((m x x@0))), \mneg{}(snd((m x x@0)))>))\000C
(\mlambda{}I,rho. 0 \mvee{} dM-to-FL(I;\mneg{}(snd(rho))))
(\mlambda{}I,rho. if (0==1)
then \mcdot{}
else snd(fst((m I rho)))
fi )
(\mlambda{}I,a. (snd(fst(a))))
I
<fst(a@0), \mneg{}(snd(a@0))>) in
\mlambda{}I,a@0,J,f,u@0,J@0,f@0,u@1.
(cA H.((A)sigma)[1(\mBbbI{})].\mBbbI{}
(\mlambda{}x,x@0. (sigma x
<fst(fst(fst(x@0)))
, snd(x@0)
>))
(\mlambda{}I,rho.
phi I (fst(fst(rho))) \mvee{} ...)
(\mlambda{}I,rho.
if (phi I
(fst(fst(fst(rho))))==1)
then (snd((u I
<fst(fst(...))
, snd(rho)
>)))
I
1
(v I
<fst(fst(rho))
, snd(rho)
>)
I
1
(snd(fst(rho)))
if (dM-to-FL(I;\mneg{}(...))==1)
then a I
<fst(fst(fst(rho)))
, snd(rho)
>
else v I
<fst(fst(rho))
, snd(rho)
>
fi )
(\mlambda{}I,a. ((snd((a0 I (fst(fst(a))))))
I
1
(v I <fst(a), 0>)
I
1
(snd(a))))
J@0
<f@0((f(a@0);u@0)), u@1>) in
cubical-pair(\mlambda{}I,a@0. (a I <a@0, 1(\mBbbI{}) I a@0>);b))
By
Latex:
((UnivCD THENA Auto)
THEN SqEqualTopToBase
THEN Unfold `contractible\_comp` 0
THEN RepUR ``path\_comp path\_term path-term comp-term comp\_term`` 0
THEN ...
THEN ...
THEN RepUR ``csm-comp-structure csm-comp compose face-or cubical-term-at face-one`` 0)
Home
Index