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 a f)
, 
presheaf-type-ap-morph: (u a 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