Nuprl Lemma : path-type-subset-adjoin3

[X,T1,T2,T3,A,w,a,phi:Top].  ((X, phi.T1.T2.T3 ⊢ Path_A w) (X.T1.T2.T3 ⊢ Path_A w))


Proof




Definitions occuring in Statement :  path-type: (Path_A b) context-subset: Gamma, phi cube-context-adjoin: X.A uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] path-type: (Path_A b) cubical-subset: {t:T | ∀I,alpha. psi[I; alpha; t]} pathtype: Path(A) cube-context-adjoin: X.A cubical-fun: (A ⟶ B) context-subset: Gamma, phi all: x:A. B[x] member: t ∈ T top: Top cubical-fun-family: cubical-fun-family(X; A; B; I; a) pi1: fst(t) pi2: snd(t)
Lemmas referenced :  cubical_type_at_pair_lemma I_cube_pair_redex_lemma cube_set_restriction_pair_lemma cubical_type_ap_morph_pair_lemma top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation sqequalRule cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis because_Cache

Latex:
\mforall{}[X,T1,T2,T3,A,w,a,phi:Top].    ((X,  phi.T1.T2.T3  \mvdash{}  Path\_A  a  w)  \msim{}  (X.T1.T2.T3  \mvdash{}  Path\_A  a  w))



Date html generated: 2017_01_10-AM-08_52_51
Last ObjectModification: 2016_12_11-PM-02_10_45

Theory : cubical!type!theory


Home Index