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