Nuprl Lemma : cubical-term-equal2

[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[u,z:{X ⊢ _:A}].
  z ∈ {X ⊢ _:A} supposing ∀I:Cname List. ∀a:X(I).  ((u a) (z a) ∈ ((fst(A)) a))


Proof




Definitions occuring in Statement :  cubical-term: {X ⊢ _:AF} cubical-type: {X ⊢ _} I-cube: X(I) cubical-set: CubicalSet coordinate_name: Cname list: List uimplies: supposing a uall: [x:A]. B[x] pi1: fst(t) all: x:A. B[x] apply: a equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] cubical-type: {X ⊢ _} pi1: fst(t) cubical-term: {X ⊢ _:AF} uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s] prop: guard: {T}
Lemmas referenced :  cubical-term_wf cubical-type_wf cubical-set_wf I-cube_wf list_wf coordinate_name_wf all_wf equal_wf name-morph_wf cube-set-restriction_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaFormation setElimination rename productElimination sqequalRule applyEquality introduction lambdaEquality dependent_functionElimination because_Cache isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry dependent_set_memberEquality functionExtensionality

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[u,z:\{X  \mvdash{}  \_:A\}].
    u  =  z  supposing  \mforall{}I:Cname  List.  \mforall{}a:X(I).    ((u  I  a)  =  (z  I  a))



Date html generated: 2016_06_16-PM-05_40_18
Last ObjectModification: 2015_12_28-PM-04_35_33

Theory : cubical!sets


Home Index