Nuprl Lemma : constant-cubical-type-at

[X,I,a:Top].  ((X)(a) X(I))


Proof




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

Latex:
\mforall{}[X,I,a:Top].    ((X)(a)  \msim{}  X(I))



Date html generated: 2016_06_16-PM-05_48_18
Last ObjectModification: 2015_12_28-PM-04_31_46

Theory : cubical!sets


Home Index