Nuprl Lemma : csm-adjoin-wf

[Gamma,Delta:j⊢]. ∀[A:{Gamma ⊢_}]. ∀[sigma:Delta j⟶ Gamma]. ∀[u:{Delta ⊢ _:(A)sigma}].
  ((sigma;u) ∈ Delta ij⟶ Gamma.A)


Proof




Definitions occuring in Statement :  csm-adjoin: (s;u) cube-context-adjoin: X.A cubical-term: {X ⊢ _:A} csm-ap-type: (AF)s cubical-type: {X ⊢ _} cube_set_map: A ⟶ B cubical_set: CubicalSet uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T cubical_set: CubicalSet cube_set_map: A ⟶ B csm-ap-type: (AF)s pscm-ap-type: (AF)s csm-ap: (s)x pscm-ap: (s)x cube-context-adjoin: X.A psc-adjoin: X.A I_cube: A(I) I_set: A(I) cubical-type-at: A(a) presheaf-type-at: A(a) cube-set-restriction: f(s) psc-restriction: f(s) cubical-type-ap-morph: (u f) presheaf-type-ap-morph: (u f) csm-adjoin: (s;u) pscm-adjoin: (s;u)
Lemmas referenced :  pscm-adjoin-wf cube-cat_wf cubical-type-sq-presheaf-type cubical-term-sq-presheaf-term
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesis sqequalRule instantiate Error :memTop

Latex:
\mforall{}[Gamma,Delta:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}'  \_\}].  \mforall{}[sigma:Delta  j{}\mrightarrow{}  Gamma].  \mforall{}[u:\{Delta  \mvdash{}  \_:(A)sigma\}].
    ((sigma;u)  \mmember{}  Delta  ij{}\mrightarrow{}  Gamma.A)



Date html generated: 2020_05_20-PM-01_56_13
Last ObjectModification: 2020_04_04-AM-09_36_44

Theory : cubical!type!theory


Home Index