Nuprl Lemma : cc-fstfst_wf

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


Proof




Definitions occuring in Statement :  cc-fstfst: pp cube-context-adjoin: 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-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) cube_set_map: A ⟶ B cc-fstfst: pp psc-fstfst: pp
Lemmas referenced :  psc-fstfst_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{}  \_\}].  \mforall{}[B:\{Gamma.A  \mvdash{}  \_\}].    (pp  \mmember{}  Gamma.A.B  ij{}\mrightarrow{}  Gamma)



Date html generated: 2020_05_20-PM-01_55_10
Last ObjectModification: 2020_04_04-AM-09_29_35

Theory : cubical!type!theory


Home Index