Nuprl Lemma : transEquiv-trans-sq
∀[G,A,p,I,a,J,f,u:Top].
(transEquivFun(p) I a J f u ~ let x,cA = p I+new-name(I) 1(s(1(a))) I+new-name(I) 1 <new-name(I)>
in cA J new-name(J)
1 ⋅ cube+(I;new-name(I)) J+new-name(J) <1 ⋅ f ⋅ s, 1 ∧ <new-name(J)>> ⋅ 1
(0)<1 ⋅ f> ∨ 0
(λI@1,a@0. (if ((0)<1 ⋅ f ⋅ s ⋅ a@0>==1) then (fst(⋅)) I@1 1 else λu.u fi
((snd((A I@1+new-name(I@1)
cube+(I;new-name(I)) I@1+new-name(I@1)
<1 ⋅ f ⋅ s ⋅ a@0 ⋅ s
, 1 ∧ ¬(dM-lift(I@1+new-name(I@1);I@1;s)
¬(dM-lift(I@1;J+new-name(J);a@0)
<new-name(J)>) ∧ <new-name(I@1)>)
>(1(1(1(s(1(a)))))))))
I@1
new-name(I@1)
1
0 ∨ dM-to-FL(I@1;¬(¬(dM-lift(I@1;J+new-name(J);a@0) <new-name(J)>)))
(λI@0,a@1. ((((u 1 s) 1 a@0) 1 s) 1 a@1))
((u 1 s) 1 a@0))))
((snd((A J+new-name(J)
cube+(I;new-name(I)) J+new-name(J) <1 ⋅ f ⋅ s, 1 ∧ ¬(1 ∧ <new-name(J)>)>(1(1(1\000C(s(1(a)))))))))
J
new-name(J)
1
0
(λI@1,a@0. ((u 1 s) 1 a@0))
u))
Proof
Definitions occuring in Statement :
transEquiv-trans: transEquivFun(p),
csm-m: m,
cube+: cube+(I;i),
interval-1: 1(𝕀),
interval-type: 𝕀,
csm-id-adjoin: [u],
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
fl-morph: <f>,
dM-to-FL: dM-to-FL(I;z),
fl-eq: (x==y),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
nc-s: s,
new-name: new-name(I),
add-name: I+i,
nh-comp: g ⋅ f,
nh-id: 1,
dM-lift: dM-lift(I;J;f),
names-hom: I ⟶ J,
dM1: 1,
dM_inc: <x>,
dM: dM(I),
names-deq: NamesDeq,
names: names(I),
ifthenelse: if b then t else f fi ,
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>,
product: x:A × B[x],
sqequal: s ~ t,
dma-neg: ¬(x),
dm-neg: ¬(x),
lattice-0: 0,
lattice-1: 1,
lattice-join: a ∨ b,
lattice-meet: a ∧ b
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
transEquiv-trans: transEquivFun(p),
transEquiv: transEquiv{i:l}(G;A;p),
equiv-fun: equiv-fun(f),
cubical-subst: cubical-subst(G;f;pth;x),
cubical-fst: p.1,
cubical-app: app(w; u),
cubical-id-equiv: IdEquiv(X;T),
equiv-witness: equiv-witness(f;cntr),
cubical-pair: cubical-pair(u;v),
path-trans: PathTransport(p),
univ-trans: univ-trans(G;T),
transprt-fun: transprt-fun(Gamma;A;cA),
cubical-lambda: (λb),
universe-decode: decode(t),
cube-context-adjoin: X.A,
map-path: map-path(G;f;pth),
path-eta: path-eta(pth),
universe-comp-op: compOp(t),
all: ∀x:A. B[x],
member: t ∈ T,
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s,
cubicalpath-app: pth @ r,
cubical-lam: cubical-lam(X;b),
term-to-path: <>(a),
csm-ap-type: (AF)s,
csm-comp-structure: (cA)tau,
transprt: transprt(G;cA;a0),
comp-op-to-comp-fun: cop-to-cfun(cA),
csm-id-adjoin: [u],
cubical-id-fun: cubical-id-fun(X),
cc-adjoin-cube: (v;u),
csm-ap: (s)x,
csm+: tau+,
csm-comp: G o F,
pi1: fst(t),
pi2: snd(t),
csm-id: 1(X),
csm-adjoin: (s;u),
compose: f o g,
cubical-term-at: u(a),
face-0: 0(𝔽),
equivTerm: equivTerm(G;A;B),
csm-composition: (comp)sigma,
composition-term: comp cA [phi ⊢→ u] a0,
comp_term: comp cA [phi ⊢→ u] a0,
equiv-comp: equiv-comp(H;A;E;cA;cE),
universe-encode: encode(T;cT),
discrete-cubical-term: discr(t),
context-map: <rho>,
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
comp-fun-to-comp-op1: comp-fun-to-comp-op1(Gamma;A;comp),
canonical-section: canonical-section(Gamma;A;I;rho;a),
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
equiv_comp_apply: equiv_comp_apply(H;A;E;cA;cE;I;a;b;c;d),
cubical-type-ap-morph: (u a f),
cubical-universe: c𝕌,
closed-type-to-type: closed-type-to-type(T),
closed-cubical-universe: cc𝕌,
csm-fibrant-type: csm-fibrant-type(G;H;s;FT),
so_lambda: so_lambda4,
so_apply: x[s1;s2;s3;s4],
uimplies: b supposing a,
label: ...$L... t,
cube-set-restriction: f(s),
csm-m: m,
formal-cube: formal-cube(I),
cubical-equiv: Equiv(T;A),
cubical-fun: (A ⟶ B),
cubical-sigma: Σ A B,
subset-iota: iota,
interval-1: 1(𝕀),
dma-neg: ¬(x),
record-select: r.x,
dM: dM(I),
free-DeMorgan-algebra: free-DeMorgan-algebra(T;eq),
mk-DeMorgan-algebra: mk-DeMorgan-algebra(L;n),
record-update: r[x := v],
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
btrue: tt,
dm-neg: ¬(x),
lattice-extend: lattice-extend(L;eq;eqL;f;ac),
lattice-fset-join: \/(s),
reduce: reduce(f;k;as),
list_ind: list_ind,
fset-image: f"(s),
f-union: f-union(domeq;rngeq;s;x.g[x]),
list_accum: list_accum,
dM0: 0,
lattice-0: 0,
bfalse: ff,
free-DeMorgan-lattice: free-DeMorgan-lattice(T;eq),
free-dist-lattice: free-dist-lattice(T; eq),
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o),
empty-fset: {},
nil: [],
it: ⋅,
opposite-lattice: opposite-lattice(L),
lattice-1: 1,
fset-singleton: {x},
cons: [a / b],
dM1: 1,
fset-union: x ⋃ y,
l-union: as ⋃ bs,
insert: insert(a;L),
eval_list: eval_list(t),
deq-member: x ∈b L,
lattice-join: a ∨ b,
lattice-meet: a ∧ b,
fset-ac-glb: fset-ac-glb(eq;ac1;ac2),
fset-minimals: fset-minimals(x,y.less[x; y]; s),
fset-filter: {x ∈ s | P[x]},
filter: filter(P;l),
lattice-fset-meet: /\(s),
dM-to-FL: dM-to-FL(I;z),
face_lattice: face_lattice(I),
face-lattice: face-lattice(T;eq),
free-dist-lattice-with-constraints: free-dist-lattice-with-constraints(T;eq;x.Cs[x]),
constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P),
fset-constrained-ac-lub: lub(P;ac1;ac2),
fset-ac-lub: fset-ac-lub(eq;ac1;ac2)
Lemmas referenced :
I_cube_pair_redex_lemma,
cube_set_restriction_pair_lemma,
cubical_type_at_pair_lemma,
cubical_type_ap_morph_pair_lemma,
arrow_pair_lemma,
equiv_comp-apply-sq,
istype-top,
lifting-strict-spread,
strict4-spread,
strict4-apply,
interval-type-ap-morph,
lifting-strict-ifthenelse,
face-type-ap-morph,
dM-lift-1-sq
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
sqequalRule,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
Error :memTop,
hypothesis,
isectElimination,
hypothesisEquality,
because_Cache,
inhabitedIsType,
baseClosed,
independent_isectElimination,
lambdaFormation_alt
Latex:
\mforall{}[G,A,p,I,a,J,f,u:Top].
(transEquivFun(p) I a J f u
\msim{} let x,cA = p I+new-name(I) 1(s(1(a))) I+new-name(I) 1 <new-name(I)>
in cA J new-name(J) 1 \mcdot{} cube+(I;new-name(I)) J+new-name(J) ə \mcdot{} f \mcdot{} s, 1 \mwedge{} <new-name(J)>> \mcdot{} 1 (0\000C)ə \mcdot{} f> \mvee{} 0
(\mlambda{}I@1,a@0. (if ((0)ə \mcdot{} f \mcdot{} s \mcdot{} a@0>==1) then (fst(\mcdot{})) I@1 1 else \mlambda{}u.u fi
((snd((A I@1+new-name(I@1)
cube+(I;new-name(I)) I@1+new-name(I@1)
ə \mcdot{} f \mcdot{} s \mcdot{} a@0 \mcdot{} s
, 1 \mwedge{} \mneg{}(dM-lift(I@1+new-name(I@1);I@1;s)
\mneg{}(dM-lift(I@1;J+new-name(J);a@0) <new-name(J)>) \mwedge{} <new-name(I@1)>)
>(1(1(1(s(1(a)))))))))
I@1
new-name(I@1)
1
0 \mvee{} dM-to-FL(I@1;\mneg{}(\mneg{}(dM-lift(I@1;J+new-name(J);a@0) <new-name(J)>)))
(\mlambda{}I@0,a@1. ((((u 1 s) 1 a@0) 1 s) 1 a@1))
((u 1 s) 1 a@0))))
((snd((A J+new-name(J)
cube+(I;new-name(I)) J+new-name(J) ə \mcdot{} f \mcdot{} s, 1 \mwedge{} \mneg{}(1 \mwedge{} <new-name(J)>)>(1(1(1(s(1(a))\000C)))))))
J
new-name(J)
1
0
(\mlambda{}I@1,a@0. ((u 1 s) 1 a@0))
u))
Date html generated:
2020_05_20-PM-07_35_36
Last ObjectModification:
2020_04_25-PM-10_42_10
Theory : cubical!type!theory
Home
Index