Nuprl Lemma : path-trans-sq
∀[G,pth,I,a,J,h,u:Top]. (PathTransport(pth) I a J h u ~ compOp(path-eta(pth)) J new-name(J) <s(h(a)), <new-name(J)>> 0 \000Cdiscr(⋅) u)
Proof
Definitions occuring in Statement :
path-trans: PathTransport(p),
universe-comp-op: compOp(t),
path-eta: path-eta(pth),
discrete-cubical-term: discr(t),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
nc-s: s,
new-name: new-name(I),
add-name: I+i,
dM_inc: <x>,
it: ⋅,
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
pair: <a, b>,
sqequal: s ~ t,
lattice-0: 0
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
path-trans: PathTransport(p),
univ-trans: univ-trans(G;T),
transprt-fun: transprt-fun(Gamma;A;cA),
cubical-lambda: (λb),
member: t ∈ T,
interval-0: 0(𝕀),
cc-snd: q,
csm-id-adjoin: [u],
csm-ap-term: (t)s,
cc-fst: p,
csm-id: 1(X),
csm-adjoin: (s;u),
csm-ap: (s)x,
pi1: fst(t),
pi2: snd(t),
cubicalpath-app: pth @ r,
cubical-app: app(w; u),
csm+: tau+,
csm-comp-structure: (cA)tau,
transprt: transprt(G;cA;a0),
csm-comp: G o F,
comp_term: comp cA [phi ⊢→ u] a0,
compose: f o g,
comp-op-to-comp-fun: cop-to-cfun(cA),
csm-composition: (comp)sigma,
cc-adjoin-cube: (v;u),
face-0: 0(𝔽),
composition-term: comp cA [phi ⊢→ u] a0,
discrete-cubical-term: discr(t),
cubical-term-at: u(a),
cube-context-adjoin: X.A,
all: ∀x:A. B[x]
Lemmas referenced :
istype-top,
cube_set_restriction_pair_lemma,
csm-universe-decode,
csm-path-eta
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
sqequalRule,
because_Cache,
inhabitedIsType,
hypothesisEquality,
cut,
introduction,
extract_by_obid,
hypothesis,
Error :memTop,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isectElimination
Latex:
\mforall{}[G,pth,I,a,J,h,u:Top].
(PathTransport(pth) I a J h u \msim{} compOp(path-eta(pth)) J new-name(J) <s(h(a)), <new-name(J)>> 0 dis\000Ccr(\mcdot{}) u)
Date html generated:
2020_05_20-PM-07_32_47
Last ObjectModification:
2020_04_25-PM-10_33_05
Theory : cubical!type!theory
Home
Index