Nuprl Lemma : contractible_comp-apply-sq
∀[X,A,cA,B,a,b,c,d,J,x:Top].
(contractible_comp(X;A;cA) B (λx,y. a[x;y]) (λx,y. b[x;y]) (λx,y. c[x;y]) (λx,y. d[x;y]) J x
~ <cA <λI.(alpha:B(I) × 𝕀(alpha)), λI,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>> (λx,x@0. a[x;m x x@0])
(λI,rho. b[I;fst(rho)] ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. if (b[I;fst((m I rho))]==1) then fst(c[I;m I rho]) else fst(d[I;fst((m I rho))]) fi )
(λI,a. (fst(d[I;fst(a)])))
J
<x, 1>
, λJ@0,f,u@0,J@1,f@0,u@1. (cA
<λI.(alpha:alpha:B(I) × ((A)λx,y. a[x;y])[λI,rho. 1](alpha) × 𝕀(alpha))
, λI,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)>, (snd(p) fst(p) f)>
>
(λx,x@0. a[x;<fst(fst(fst(x@0))), snd(x@0)>])
(λI,rho. b[I;fst(fst(rho))] ∨ dM-to-FL(I;¬(snd(rho))) ∨ dM-to-FL(I;snd(rho)))
(λI,rho. if (b[I;fst(fst(fst(rho)))]==1)
then (snd(c[I;<fst(fst(fst(rho))), snd(rho)>])) I 1
(cA
<λI.(alpha:alpha:B(I) × ((A)λx,y. a[x;y])[λI,rho. 1](alpha) × 𝕀(alpha))
, λI,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)>
, (snd(p) fst(p) f)
>
>
(λx,x@0. a[x;<fst(fst((m x x@0))), ¬(snd((m x x@0)))>])
(λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. (snd(fst((m I rho)))))
(λI,a. (snd(fst(a))))
I
<fst(fst(rho)), ¬(snd(rho))>)
I
1
(snd(fst(rho)))
if (dM-to-FL(I;¬(snd(fst(rho))))==1)
then cA <λI.(alpha:B(I) × 𝕀(alpha)), λI,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>>
(λx,x@0. a[x;m x x@0])
(λI,rho. b[I;fst(rho)] ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. if (b[I;fst((m I rho))]==1)
then fst(c[I;m I rho])
else fst(d[I;fst((m I rho))])
fi )
(λI,a. (fst(d[I;fst(a)])))
I
<fst(fst(fst(rho))), snd(rho)>
else cA
<λI.(alpha:alpha:B(I) × ((A)λx,y. a[x;y])[λI,rho. 1](alpha) × 𝕀(alpha))
, λI,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)>
, (snd(p) fst(p) f)
>
>
(λx,x@0. a[x;<fst(fst((m x x@0))), ¬(snd((m x x@0)))>])
(λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. (snd(fst((m I rho)))))
(λI,a. (snd(fst(a))))
I
<fst(fst(rho)), ¬(snd(rho))>
fi )
(λI,a@0. ((snd(d[I;fst(fst(a@0))])) I 1
(cA
<λI.(alpha:alpha:B(I) × ((A)λx,y. a[x;y])[λI,rho. 1](alpha) × 𝕀(alpha))
, λI,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)>, (snd(p) fst(p) f)>
>
(λx,x@0. a[x;<fst(fst((m x x@0))), ¬(snd((m x x@0)))>])
(λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. (snd(fst((m I rho)))))
(λI,a. (snd(fst(a))))
I
<fst(a@0), ¬(0)>)
I
1
(snd(a@0))))
J@1
<<f@0(f(x)), (u@0 f(x) f@0)>, u@1>)
>)
Proof
Definitions occuring in Statement :
contractible_comp: contractible_comp(X;A;cA),
csm-m: m,
interval-type: 𝕀,
csm-id-adjoin: [u],
csm-ap-type: (AF)s,
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
dM-to-FL: dM-to-FL(I;z),
fl-eq: (x==y),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
I_cube: A(I),
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 ,
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s1;s2],
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
product: x:A × B[x],
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
top: Top,
let: let,
pi1: fst(t),
pi2: snd(t),
ifthenelse: if b then t else f fi ,
bfalse: ff,
cc-adjoin-cube: (v;u),
cube-context-adjoin: X.A,
interval-1: 1(𝕀),
cubical-pair: cubical-pair(u;v),
all: ∀x:A. B[x]
Lemmas referenced :
contractible_comp-sq,
Error :cube_set_restriction_pair_lemma,
top_wf,
fl-eq-0-1-false
Rules used in proof :
cut,
sqequalRule,
thin,
sqequalSubstitution,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
because_Cache,
dependent_functionElimination,
isect_memberFormation,
sqequalAxiom,
hypothesisEquality
Latex:
\mforall{}[X,A,cA,B,a,b,c,d,J,x:Top].
(contractible\_comp(X;A;cA) B (\mlambda{}x,y. a[x;y]) (\mlambda{}x,y. b[x;y]) (\mlambda{}x,y. c[x;y]) (\mlambda{}x,y. d[x;y]) J x
\msim{} <cA <\mlambda{}I.(alpha:B(I) \mtimes{} \mBbbI{}(alpha)), \mlambda{}I,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>> (\mlambda{}x,x@0. a[x;m x x@0]\000C)
(\mlambda{}I,rho. b[I;fst(rho)] \mvee{} dM-to-FL(I;\mneg{}(snd(rho))))
(\mlambda{}I,rho. if (b[I;fst((m I rho))]==1) then fst(c[I;m I rho]) else fst(d[I;fst((m I rho))]) fi )
(\mlambda{}I,a. (fst(d[I;fst(a)])))
J
<x, 1>
, \mlambda{}J@0,f,u@0,J@1,f@0,u@1.
(cA
<\mlambda{}I.(alpha:alpha:B(I) \mtimes{} ((A)\mlambda{}x,y. a[x;y])[\mlambda{}I,rho. 1](alpha) \mtimes{} \mBbbI{}(alpha)\000C)
, \mlambda{}I,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)>
, (snd(p) fst(p) f)
>
>
(\mlambda{}x,x@0. a[x;<fst(fst(fst(x@0))), snd(x@0)>])
(\mlambda{}I,rho.
b
[I;fst(fst(rho))] \mvee{} dM-to-FL(I;\mneg{}(snd(rho))) \mvee{} dM-to-FL(I;...))\000C
(\mlambda{}I,rho. if (b[I;fst(fst(fst(rho)))]==1)
then (snd(c[I;<fst(fst(fst(rho))), snd(rho)>])) I 1
(cA
<\mlambda{}I.(alpha:alpha:B(I) \mtimes{} ((A)\mlambda{}x,y. a[x;y])[\mlambda{}I,rho. 1](\000Calpha)
\mtimes{} \mBbbI{}(alpha))
, \mlambda{}I,J,f,p. <<f(fst(fst(p)))
, (snd(fst(p)) fst(fst(p)) f)
>
, (snd(p) fst(p) f)
>
>
(\mlambda{}x,x@0. a[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. (snd(fst((m I rho)))))
(\mlambda{}I,a. (snd(fst(a))))
I
<fst(fst(rho)), \mneg{}(snd(rho))>)
I
1
(snd(fst(rho)))
if (dM-to-FL(I;\mneg{}(snd(fst(rho))))==1)
then cA
<\mlambda{}I.(alpha:B(I) \mtimes{} \mBbbI{}(alpha))
, \mlambda{}I,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>
>
(\mlambda{}x,x@0. a[x;m x x@0])
(\mlambda{}I,rho. b[I;fst(rho)] \mvee{} dM-to-FL(I;\mneg{}(snd(rho))))
(\mlambda{}I,rho. if (b[I;fst((m I rho))]==1)
then fst(c[I;m I rho])
else fst(d[I;fst((m I rho))])
fi )
(\mlambda{}I,a. (fst(d[I;fst(a)])))
I
<fst(fst(fst(rho))), snd(rho)>
else cA
<\mlambda{}I.(alpha:alpha:B(I) \mtimes{} ((A)\mlambda{}x,y. a[x;y])[\mlambda{}I,rho. 1](alph\000Ca)
\mtimes{} \mBbbI{}(alpha))
, \mlambda{}I,J,f,p. <<f(fst(fst(p)))
, (snd(fst(p)) fst(fst(p)) f)
>
, (snd(p) fst(p) f)
>
>
(\mlambda{}x,x@0. a[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. (snd(fst((m I rho)))))
(\mlambda{}I,a. (snd(fst(a))))
I
<fst(fst(rho)), \mneg{}(snd(rho))>
fi )
(\mlambda{}I,a@0. ((snd(d[I;fst(fst(a@0))])) I 1
(cA
<\mlambda{}I.(alpha:alpha:B(I) \mtimes{} ((A)\mlambda{}x,y. a[x;y])[\mlambda{}I,rho. 1](alpha)
\mtimes{} \mBbbI{}(alpha))
, \mlambda{}I,J,f,p. <<f(fst(fst(p))), (snd(fst(p)) fst(fst(p)) f)>
, (snd(p) fst(p) f)
>
>
(\mlambda{}x,x@0. a[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. (snd(fst((m I rho)))))
(\mlambda{}I,a. (snd(fst(a))))
I
<fst(a@0), \mneg{}(0)>)
I
1
(snd(a@0))))
J@1
<<f@0(f(x)), (u@0 f(x) f@0)>, u@1>)
>)
Date html generated:
2018_05_23-AM-11_03_48
Last ObjectModification:
2017_11_24-PM-05_26_33
Theory : cubical!type!theory
Home
Index