Nuprl Lemma : interval-type-at

[J,rho:Top].  (𝕀(rho) ~ 𝕀(J))


Proof




Definitions occuring in Statement :  interval-type: 𝕀 cubical-type-at: A(a) interval-presheaf: 𝕀 I_cube: A(I) uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T interval-type: 𝕀 top: Top
Lemmas referenced :  top_wf constant-cubical-type-at
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesisEquality hypothesis sqequalAxiom because_Cache

Latex:
\mforall{}[J,rho:Top].    (\mBbbI{}(rho)  \msim{}  \mBbbI{}(J))



Date html generated: 2016_05_18-PM-01_59_56
Last ObjectModification: 2016_03_03-PM-02_29_15

Theory : cubical!type!theory


Home Index