Nuprl Lemma : cube-context-adjoin_wf

[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}].  Gamma.A ij⊢


Proof




Definitions occuring in Statement :  cube-context-adjoin: X.A cubical-type: {X ⊢ _} 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-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)
Lemmas referenced :  psc-adjoin_wf cube-cat_wf cubical-type-sq-presheaf-type
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{}  \_\}].    Gamma.A  ij\mvdash{}



Date html generated: 2020_05_20-PM-01_54_27
Last ObjectModification: 2020_04_04-AM-09_36_55

Theory : cubical!type!theory


Home Index