Nuprl 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))
Proof
Definitions occuring in Statement :
contractible_comp: contractible_comp(X;A;cA),
csm-m: m,
interval-1: 1(𝕀),
interval-type: 𝕀,
cubical-pair: cubical-pair(u;v),
csm-id-adjoin: [u],
cc-adjoin-cube: (v;u),
cube-context-adjoin: X.A,
csm-ap-type: (AF)s,
dM-to-FL: dM-to-FL(I;z),
fl-eq: (x==y),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
nh-id: 1,
dM1: 1,
dM0: 0,
dM: dM(I),
names-deq: NamesDeq,
names: names(I),
dma-neg: ¬(x),
dm-neg: ¬(x),
lattice-0: 0,
lattice-1: 1,
lattice-join: a ∨ b,
ifthenelse: if b then t else f fi ,
let: let,
it: ⋅,
uall: ∀[x:A]. B[x],
top: Top,
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
contractible_comp: contractible_comp(X;A;cA),
path_comp: path_comp,
path_term: path_term(phi; w; a; b; r),
comp_term: comp cA [phi ⊢→ u] a0,
path-term: path-term(phi;w;a;b;r),
cc-adjoin-cube: (v;u),
csm-ap-term: (t)s,
cubical-path-app: pth @ r,
term-to-path: <>(a),
csm-ap: (s)x,
cubicalpath-app: pth @ r,
cubical-lambda: (λb),
cubical-app: app(w; u),
cc-snd: q,
cc-fst: p,
csm+: tau+,
face-zero: (i=0),
case-term: (u ∨ v),
csm-comp: G o F,
csm-adjoin: (s;u),
cubical-term-at: u(a),
compose: f o g,
face-one: (i=1),
face-or: (a ∨ b),
csm-comp-structure: (cA)tau,
csm-id: 1(X),
pi_comp: pi_comp(X;A;cA;cB),
revfill: revfill(Gamma;cA;a1),
rev_fill_term: rev_fill_term(Gamma;cA;phi;u;a1),
rev-type-comp: rev-type-comp(Gamma;cA),
fill_term: fill cA [phi ⊢→ u] a0,
comp-to-fill: comp-to-fill(Gamma;cA),
discrete-cubical-term: discr(t),
face-0: 0(𝔽),
pi1: fst(t),
pi2: snd(t),
interval-rev: 1-(r),
csm-id-adjoin: [u],
interval-0: 0(𝕀),
sigma_comp: sigma_comp(cA;cB),
cubical-snd: p.2,
cubical-fst: p.1,
all: ∀x:A. B[x],
csm-ap-type: (AF)s,
interval-1: 1(𝕀),
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s1;s2;s3;s4],
so_lambda: λ2x y.t[x; y],
top: Top,
so_apply: x[s1;s2],
uimplies: b supposing a
Lemmas referenced :
top_wf,
lifting-strict-spread,
strict4-spread
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
thin,
sqequalHypSubstitution,
hypothesis,
sqequalAxiom,
extract_by_obid,
isect_memberEquality,
isectElimination,
hypothesisEquality,
because_Cache,
lambdaFormation,
baseClosed,
voidElimination,
voidEquality,
independent_isectElimination,
dependent_functionElimination
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))
Date html generated:
2018_05_23-AM-11_03_33
Last ObjectModification:
2017_11_24-PM-02_15_02
Theory : cubical!type!theory
Home
Index