Nuprl Lemma : cubical-fiber-subset-adjoin2

[X,T,A,B1,B2,w,a,phi:Top].  (X, phi.B1.B2 ⊢ Fiber(w;a) X.B1.B2 ⊢ Fiber(w;a))


Proof




Definitions occuring in Statement :  cubical-fiber: Fiber(w;a) context-subset: Gamma, phi cube-context-adjoin: X.A uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  cubical-fiber: Fiber(w;a) cubical-sigma: Σ B uall: [x:A]. B[x] member: t ∈ T top: Top
Lemmas referenced :  path-type-subset-adjoin3 top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality voidElimination voidEquality hypothesis because_Cache isect_memberFormation sqequalAxiom

Latex:
\mforall{}[X,T,A,B1,B2,w,a,phi:Top].    (X,  phi.B1.B2  \mvdash{}  Fiber(w;a)  \msim{}  X.B1.B2  \mvdash{}  Fiber(w;a))



Date html generated: 2017_01_10-AM-08_56_36
Last ObjectModification: 2016_12_11-PM-02_17_13

Theory : cubical!type!theory


Home Index