Nuprl Lemma : I-path_wf

[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)].  (I-path(X;A;a;b;I;alpha) ∈ Type)


Proof




Definitions occuring in Statement :  I-path: I-path(X;A;a;b;I;alpha) cubical-term: {X ⊢ _:AF} cubical-type: {X ⊢ _} I-cube: X(I) cubical-set: CubicalSet coordinate_name: Cname list: List uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T I-path: I-path(X;A;a;b;I;alpha) prop: all: x:A. B[x] uimplies: supposing a
Lemmas referenced :  coordinate_name_wf not_wf l_member_wf named-path_wf I-cube_wf list_wf cubical-term_wf cubical-type_wf cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule productEquality setEquality lemma_by_obid hypothesis sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality lambdaFormation setElimination rename independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[I:Cname  List].  \mforall{}[alpha:X(I)].
    (I-path(X;A;a;b;I;alpha)  \mmember{}  Type)



Date html generated: 2016_06_16-PM-07_28_44
Last ObjectModification: 2015_12_28-PM-04_14_03

Theory : cubical!sets


Home Index