Nuprl Lemma : pi_comp-sq
∀[X,A,cA,cB:Top].
(pi_comp(X;A;cA;cB) ~ λH,sigma,phi,u,a0. let v = λI,a. (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. (snd(fst((m I rho)))))
(λI,a. (snd(fst(a))))
I
<fst(a), ¬(snd(a))>) in
(λcB H.((A)sigma)[1(𝕀)] (λx,x@0. <sigma x <fst(fst(x@0)), snd(x@0)>, v x \000Cx@0>)
(λI,a. (phi I (fst(a))))
(λI,a. (u I <fst(fst(a)), snd(a)> I 1 (v I a)))
(λI,a. (a0 I (fst(a)) I 1 (v I <a, 0>)))))
Proof
Definitions occuring in Statement :
pi_comp: pi_comp(X;A;cA;cB),
csm-m: m,
interval-1: 1(𝕀),
interval-type: 𝕀,
cubical-lambda: (λb),
csm-id-adjoin: [u],
cube-context-adjoin: X.A,
csm-ap-type: (AF)s,
dM-to-FL: dM-to-FL(I;z),
face_lattice: face_lattice(I),
nh-id: 1,
dM0: 0,
dM: dM(I),
names-deq: NamesDeq,
names: names(I),
dma-neg: ¬(x),
dm-neg: ¬(x),
lattice-0: 0,
lattice-join: a ∨ b,
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,
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),
csm-id-adjoin: [u],
csm-ap-term: (t)s,
cc-fst: p,
cubical-app: app(w; u),
csm+: tau+,
csm-comp: G o F,
csm-adjoin: (s;u),
csm-comp-structure: (cA)tau,
comp_term: comp cA [phi ⊢→ u] a0,
cc-snd: q,
csm-ap: (s)x,
compose: f o g,
pi1: fst(t),
pi2: snd(t),
csm-id: 1(X),
interval-0: 0(𝕀),
interval-rev: 1-(r),
face-0: 0(𝔽),
case-term: (u ∨ v),
cubical-term-at: u(a),
all: ∀x:A. B[x],
top: Top,
face-zero: (i=0),
face-or: (a ∨ b),
ifthenelse: if b then t else f fi ,
bfalse: ff
Lemmas referenced :
fl-eq-0-1-false,
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
thin,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
sqequalAxiom,
isectElimination,
hypothesisEquality,
because_Cache
Latex:
\mforall{}[X,A,cA,cB:Top].
(pi\_comp(X;A;cA;cB) \msim{} \mlambda{}H,sigma,phi,u,a0. let v = \mlambda{}I,a. (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. (snd(fst((m I rho)))))
(\mlambda{}I,a. (snd(fst(a))))
I
<fst(a), \mneg{}(snd(a))>) in
(\mlambda{}cB H.((A)sigma)[1(\mBbbI{})]
(\mlambda{}x,x@0. <sigma x <fst(fst(x@0)), snd(x@0)>, v x x@\000C0>)
(\mlambda{}I,a. (phi I (fst(a))))
(\mlambda{}I,a. (u I <fst(fst(a)), snd(a)> I 1 (v I a)))
(\mlambda{}I,a. (a0 I (fst(a)) I 1 (v I <a, 0>)))))
Date html generated:
2018_05_23-AM-10_54_05
Last ObjectModification:
2017_11_24-PM-02_53_14
Theory : cubical!type!theory
Home
Index