Nuprl Lemma : equiv_comp-sq
∀[H,A,E,cA,cE:Top].
(equiv_comp(H;A;E;cA;cE)
~ sigma_comp(pi_comp(H;A;cA;λH@0,sigma,phi,u,a0. (cE H@0 (λx,x@0. (fst((sigma x x@0)))) phi u a0));
pi_comp(H.(A ⟶ E);(E)λI,p. (fst(p));λH@0,sigma,phi,u,a0. (cE H@0 (λx,x@0. (fst((sigma x x@0)))) phi u a0\000C);
contractible_comp(H.(A ⟶ E).(E)λI,p. (fst(p));Fiber(λI,a. (snd(fst(a)));λI,p. (snd(p)));
λH@0,sigma,phi,u,a0,I,a@0.
<cA H@0.𝕀 (λx,x@0. (fst(fst((sigma x (m x x@0))))))
(λI,rho. phi I (fst(rho)) ∨ dM-to-FL(I;¬(snd(rho))))\000C
(λ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))))))
I
<a@0, 1>
, λJ,f,u@0.
(cE H@0.𝕀
(λx,x@0. (fst(fst((sigma x
<fst(fst(x@0))
, snd(x@0)
>)))))
(λI,rho.
phi I (fst(rho)) ∨ ... ∨ (...=1)
I
rho)
(λI,rho.
if (phi I (fst(fst(rho)))==1)
then (snd((u I
<fst(fst(rho))
, snd(rho)
>)))
I
1
(snd(fst(rho)))
if (dM-to-FL(I;¬(snd(...)))==1)
then snd((sigma I
<fst(fst(rho))
, snd(rho)
>))
else (snd(fst((sigma I
<fst(fst(rho))
, snd(rho)
>))))
I
1
(cA H@0.𝕀
(λx,x@0.
(fst(fst((sigma x
(m x
x@0)))))\000C)
(λI,a.
(phi I
(fst(a))) ∨ (λI,p. .\000C..=0))
(λI,rho.
if (...==1)
then fst((u I
(m I
rho)))
else fst((a0 I
...))
fi )
(λI,a. (fst((a0 I
(fst(a))))))
I
<fst(fst(rho)), snd(rho)>)
fi )
(λI,a. ((snd((a0 I (fst(a))))) I 1
(snd(a))))
J
(f(a@0);u@0))
>))))
Proof
Definitions occuring in Statement :
equiv_comp: equiv_comp(H;A;E;cA;cE),
contractible_comp: contractible_comp(X;A;cA),
pi_comp: pi_comp(X;A;cA;cB),
sigma_comp: sigma_comp(cA;cB),
csm-m: m,
cubical-fiber: Fiber(w;a),
face-zero: (i=0),
face-one: (i=1),
face-or: (a ∨ b),
interval-type: 𝕀,
cubical-fun: (A ⟶ B),
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,
names-deq: NamesDeq,
names: names(I),
ifthenelse: if b then t else f fi ,
uall: ∀[x:A]. B[x],
top: Top,
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
sqequal: s ~ t,
dm-neg: ¬(x),
lattice-1: 1,
lattice-join: a ∨ b
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
equiv_comp: equiv_comp(H;A;E;cA;cE),
fiber-comp: fiber-comp(X;T;A;w;a;cT;cA),
path_comp: path_comp,
face-or: (a ∨ b),
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s,
cubical-app: app(w; u),
csm+: tau+,
csm-comp-structure: (cA)tau,
cubical-term-at: u(a),
csm-ap: (s)x,
csm-comp: G o F,
csm-adjoin: (s;u),
compose: f o g,
face-zero: (i=0),
cubical-path-app: pth @ r,
path_term: path_term(phi; w; a; b; r),
cubicalpath-app: pth @ r,
path-term: path-term(phi;w;a;b;r),
case-term: (u ∨ v),
comp_term: comp cA [phi ⊢→ u] a0,
term-to-path: <>(a),
cubical-lambda: (λb),
sigma_comp: sigma_comp(cA;cB),
cubical-pair: cubical-pair(u;v),
csm-id: 1(X),
fill_term: fill cA [phi ⊢→ u] a0,
comp-to-fill: comp-to-fill(Gamma;cA),
csm-id-adjoin: [u],
cubical-snd: p.2,
cubical-fst: p.1,
pi1: fst(t),
pi2: snd(t),
interval-1: 1(𝕀),
let: let
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
thin,
sqequalHypSubstitution,
hypothesis,
axiomSqEquality,
inhabitedIsType,
hypothesisEquality,
isect_memberEquality_alt,
isectElimination,
isectIsTypeImplies,
extract_by_obid
Latex:
\mforall{}[H,A,E,cA,cE:Top].
(equiv\_comp(H;A;E;cA;cE)
\msim{} sigma\_comp(pi\_comp(H;A;cA;\mlambda{}H@0,sigma,phi,u,a0. (cE H@0 (\mlambda{}x,x@0. (fst((sigma x x@0)))) phi u a0))\000C;
pi\_comp(H.(A {}\mrightarrow{} E);(E)\mlambda{}I,p. (fst(p));\mlambda{}H@0,sigma,phi,u,a0. (cE H@0
(\mlambda{}x,x@0. (fst((sigma x x@0))))\000C
phi
u
a0);
contractible\_comp(H.(A {}\mrightarrow{} E).(E)\mlambda{}I,p. (fst(p));
Fiber(\mlambda{}I,a. (snd(fst(a)));\mlambda{}I,p. (snd(p)));
\mlambda{}H@0,sigma,phi,u,a0,I,a@0.
<cA H@0.\mBbbI{}
(\mlambda{}x,x@0. (fst(fst((sigma x
(m x x@0)))))\000C)
(\mlambda{}I,rho.
phi I (fst(rho)) \mvee{} ...)
(\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))))))
I
<a@0, 1>
, \mlambda{}J,f,u@0.
(cE H@0.\mBbbI{}
(\mlambda{}x,x@0. (fst(...)))
(\mlambda{}I,rho.
phi I
... \mvee{} ...)
(\mlambda{}I,rho.
if (phi I
...==1)
then ...
I
1
...
...)
(\mlambda{}I,a.
((snd(...))
I
1
(snd(a))))
J
(f(a@0);u@0))
>))))
Date html generated:
2020_05_20-PM-07_18_43
Last ObjectModification:
2020_04_25-PM-09_46_57
Theory : cubical!type!theory
Home
Index