Nuprl Lemma : term-p+0

[X,Y,Z,W,t,A:Top].  (((t)p+)[0(𝕀)] ((t)[0(𝕀)])p)


Proof




Definitions occuring in Statement :  interval-0: 0(𝕀) csm+: tau+ csm-id-adjoin: [u] cc-fst: p cube-context-adjoin: X.A csm-ap-term: (t)s uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  interval-0: 0(𝕀) csm-id-adjoin: [u] csm-ap-term: (t)s cc-fst: p csm+: tau+ csm-ap: (s)x csm-id: 1(X) csm-adjoin: (s;u) cc-snd: q csm-ap-type: (AF)s csm-comp: F pi2: snd(t) compose: g pi1: fst(t) uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule isect_memberFormation introduction cut sqequalAxiom extract_by_obid hypothesis sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality because_Cache

Latex:
\mforall{}[X,Y,Z,W,t,A:Top].    (((t)p+)[0(\mBbbI{})]  \msim{}  ((t)[0(\mBbbI{})])p)



Date html generated: 2018_05_23-AM-09_29_48
Last ObjectModification: 2018_05_20-PM-06_28_33

Theory : cubical!type!theory


Home Index