Step
*
1
of Lemma
contractible_comp-sq
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)
BY
{ (...
THEN ...
THEN RepUR ``interval-rev cubical-term-at`` 0
THEN RepUR ``comp_term comp-term csm-id csm-id-adjoin csm-adjoin interval-0 csm-ap cubical-app`` 0) }
1
1. cA : Base
2. A : Base
3. X : Base
⊢ sigma_comp(cA;
λH,sigma,phi,u,a0.
let v = λI,a. (cA H.(((A)λI,p. (fst(p)))sigma)λI,a. <a, 1(𝕀) I a>.𝕀
(λx,x@0. (fst((sigma x <fst(fst((m x x@0))), ¬(snd((m x x@0)))>))))
(λI,rho. 0 ∨ (λI,p. (snd(p))=0) I rho)
(λI,rho. if (0==1) then ⋅ else snd(fst((m I rho))) fi )
(λI,a. (snd(fst(a))))
I
<fst(a), ¬(snd(a))>) in
λI,a,J,f,u@0,J@0,f@0,u@1.
(cA H.(((A)λI,p. (fst(p)))sigma)λI,a. <a, 1(𝕀) I a>.𝕀
(λx,x@0. (fst((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 u I <fst(fst(fst(rho))), snd(rho)> I 1
(v I <fst(fst(rho)), snd(rho)>)
I
1
(snd(fst(rho)))
if (dM-to-FL(I;¬(snd(fst(rho))))==1)
then snd((sigma I <fst(fst(fst(rho))), snd(rho)>)\000C)
else v I <fst(fst(rho)), snd(rho)>
fi )
(λI,a. (a0 I (fst(fst(a))) I 1 (v I <fst(a), 0>) I 1 (snd(a\000C))))
J@0
<f@0((f(a);u@0)), u@1>))
~ λ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)λI,a. <a, 1(𝕀) I a>.𝕀
(λ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)λI,a. <a, 1(𝕀) I a>.𝕀
(λ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:
1. cA : Base
2. A : Base
3. X : Base
\mvdash{} sigma\_comp(cA;
pi\_comp(X.A;(A)\mlambda{}I,p. (fst(p));\mlambda{}H,sigma,phi,u,a0. (cA H (\mlambda{}x,x@0. (fst((sigma x x@0)))) p\000Chi u a0);
\mlambda{}H,sigma,phi,u,a0,I,a,J,f,u@0.
(cA H.\mBbbI{}
(\mlambda{}x,x@0. (fst(fst((sigma x
<fst(fst((1(H.\mBbbI{}.\mBbbI{}) x x@0)))
, snd((1(H.\mBbbI{}.\mBbbI{}) x x@0))
>)))))
(\mlambda{}I,rho.
phi I (fst(rho)) \mvee{} dM-to-FL(I;...) \mvee{} ...\000C)
(\mlambda{}I,rho. if (phi I (fst(fst(rho)))==1)
then u I <fst(fst(rho)), snd(rho)> I \000C1
(snd(fst(rho)))
if (dM-to-FL(I;\mneg{}(snd(fst(rho))))==1)
then snd(fst((sigma I
<fst(fst(rho))
, snd(rho)
>)))
else snd((sigma I
<fst(fst(rho)), snd(rho)>))
fi )
(\mlambda{}I,a. (a0 I (fst(a)) I 1 (snd(a))))
J
<f(a), u@0>)))
\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)))>))
(\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 \000C)
(\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{}(snd(...)))==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:
(...
THEN ...
THEN RepUR ``interval-rev cubical-term-at`` 0
THEN RepUR ``comp\_term comp-term csm-id csm-id-adjoin csm-adjoin interval-0 csm-ap cubical-app`` 0)
Home
Index