Nuprl Lemma : sigma_comp-sq
∀[X,A,cA,cB:Top].
(sigma_comp(cA;cB) ~ λ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 = cB H (λx,x@0. <sigma x x@0, a x x@0>) phi (λI,a. (snd((u I a))))
(λI,a. (snd((a0 I a)))) in
λI,a@0. <a I <a@0, 1>, b I a@0>)
Proof
Definitions occuring in Statement :
sigma_comp: sigma_comp(cA;cB),
csm-m: m,
interval-type: 𝕀,
cube-context-adjoin: X.A,
dM-to-FL: dM-to-FL(I;z),
fl-eq: (x==y),
face_lattice: face_lattice(I),
dM1: 1,
names-deq: NamesDeq,
names: names(I),
dm-neg: ¬(x),
lattice-1: 1,
lattice-join: a ∨ b,
ifthenelse: if b then t else f fi ,
let: let,
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
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
sigma_comp: sigma_comp(cA;cB),
csm-comp-structure: (cA)tau,
comp_term: comp cA [phi ⊢→ u] a0,
fill_term: fill cA [phi ⊢→ u] a0,
comp-to-fill: comp-to-fill(Gamma;cA),
csm-id-adjoin: [u],
csm+: tau+,
csm-id: 1(X),
csm-comp: G o F,
cc-fst: p,
cc-snd: q,
csm-adjoin: (s;u),
compose: f o g,
pi2: snd(t),
csm-ap: (s)x,
pi1: fst(t),
interval-1: 1(𝕀),
csm-ap-term: (t)s,
cubical-pair: cubical-pair(u;v),
cubical-snd: p.2,
cubical-fst: p.1,
case-term: (u ∨ v),
face-zero: (i=0),
face-or: (a ∨ b),
cubical-term-at: u(a)
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
hypothesis,
sqequalAxiom,
extract_by_obid,
sqequalHypSubstitution,
isect_memberEquality,
isectElimination,
thin,
hypothesisEquality,
because_Cache
Latex:
\mforall{}[X,A,cA,cB:Top].
(sigma\_comp(cA;cB) \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 = cB H (\mlambda{}x,x@0. <sigma x x@0, a x x@0>) phi
(\mlambda{}I,a. (snd((u I a))))
(\mlambda{}I,a. (snd((a0 I a)))) in
\mlambda{}I,a@0. <a I <a@0, 1>, b I a@0>)
Date html generated:
2018_05_23-AM-10_49_00
Last ObjectModification:
2017_11_24-PM-03_06_00
Theory : cubical!type!theory
Home
Index