Nuprl Lemma : csm-id-adjoin_wf

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


Proof




Definitions occuring in Statement :  csm-id-adjoin: [u] cube-context-adjoin: X.A cubical-term: {X ⊢ _:A} 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 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-id-adjoin: [u] pscm-id-adjoin: [u] csm-adjoin: (s;u) pscm-adjoin: (s;u) csm-ap: (s)x pscm-ap: (s)x csm-id: 1(X) pscm-id: 1(X)
Lemmas referenced :  pscm-id-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 Error :memTop

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



Date html generated: 2020_05_20-PM-01_56_40
Last ObjectModification: 2020_04_04-AM-09_40_44

Theory : cubical!type!theory


Home Index