Nuprl Lemma : cubical-pi-subset

[X,phi,A,B,C:Top].  (X, phi.C ⊢ ΠX.C ⊢ ΠB)


Proof




Definitions occuring in Statement :  context-subset: Gamma, phi cubical-pi: ΠB cube-context-adjoin: X.A uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  cube-context-adjoin: X.A cubical-pi: ΠB context-subset: Gamma, phi all: x:A. B[x] member: t ∈ T top: Top cubical-pi-family: cubical-pi-family(X;A;B;I;a) uall: [x:A]. B[x]
Lemmas referenced :  I_cube_pair_redex_lemma cube_set_restriction_pair_lemma top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis because_Cache isect_memberFormation sqequalAxiom isectElimination hypothesisEquality

Latex:
\mforall{}[X,phi,A,B,C:Top].    (X,  phi.C  \mvdash{}  \mPi{}A  B  \msim{}  X.C  \mvdash{}  \mPi{}A  B)



Date html generated: 2017_01_10-AM-08_50_25
Last ObjectModification: 2016_12_11-PM-01_47_09

Theory : cubical!type!theory


Home Index