Nuprl Lemma : path-trans-sq2
∀[G,pth,I,a,J,h,u:Top].
(PathTransport(pth) I a J h u ~ (snd((pth(s(h(a))) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 discr(⋅) u)
Proof
Definitions occuring in Statement :
path-trans: PathTransport(p),
discrete-cubical-term: discr(t),
cubical-term-at: u(a),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
nc-s: s,
new-name: new-name(I),
add-name: I+i,
nh-id: 1,
dM_inc: <x>,
it: ⋅,
uall: ∀[x:A]. B[x],
top: Top,
pi2: snd(t),
apply: f a,
sqequal: s ~ t,
lattice-0: 0
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
cubical-term-at: u(a),
path-eta: path-eta(pth),
universe-comp-op: compOp(t),
cc-snd: q,
cc-fst: p,
cubicalpath-app: pth @ r,
cubical-app: app(w; u),
pi2: snd(t),
csm-ap-term: (t)s,
csm-ap: (s)x,
pi1: fst(t)
Lemmas referenced :
path-trans-sq,
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
sqequalRule,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
because_Cache,
inhabitedIsType
Latex:
\mforall{}[G,pth,I,a,J,h,u:Top].
(PathTransport(pth) I a J h u \msim{} (snd((pth(s(h(a))) J+new-name(J) 1 <new-name(J)>))) J new-name(J)
1
0
discr(\mcdot{})
u)
Date html generated:
2020_05_20-PM-07_33_03
Last ObjectModification:
2020_04_25-PM-10_33_42
Theory : cubical!type!theory
Home
Index