Nuprl Lemma : is-A-face_wf

[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[bx:A(alpha)]. ∀[f:A-face(X;A;I;alpha)].
  (is-A-face(X;A;I;alpha;bx;f) ∈ ℙ)


Proof




Definitions occuring in Statement :  is-A-face: is-A-face(X;A;I;alpha;bx;f) A-face: A-face(X;A;I;alpha) cubical-type-at: A(a) cubical-type: {X ⊢ _} I-cube: X(I) cubical-set: CubicalSet coordinate_name: Cname list: List uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T is-A-face: is-A-face(X;A;I;alpha;bx;f) A-face: A-face(X;A;I;alpha) spreadn: spread3 nameset: nameset(L)
Lemmas referenced :  equal_wf cubical-type-at_wf list-diff_wf coordinate_name_wf cname_deq_wf cons_wf nil_wf cube-set-restriction_wf face-map_wf2 cubical-type-ap-morph_wf A-face_wf I-cube_wf list_wf cubical-type_wf cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin lemma_by_obid isectElimination hypothesisEquality hypothesis because_Cache setElimination rename axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[I:Cname  List].  \mforall{}[alpha:X(I)].  \mforall{}[bx:A(alpha)].
\mforall{}[f:A-face(X;A;I;alpha)].
    (is-A-face(X;A;I;alpha;bx;f)  \mmember{}  \mBbbP{})



Date html generated: 2016_06_16-PM-05_50_50
Last ObjectModification: 2015_12_28-PM-04_30_05

Theory : cubical!sets


Home Index