Nuprl Lemma : constant-cubical-type_wf
∀[X:SmallCubicalSet]. ∀[Gamma:j⊢].  Gamma ⊢ (X)
Proof
Definitions occuring in Statement : 
constant-cubical-type: (X)
, 
cubical-type: {X ⊢ _}
, 
small_cubical_set: SmallCubicalSet
, 
cubical_set: CubicalSet
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
small_cubical_set: SmallCubicalSet
, 
cubical_set: CubicalSet
, 
constant-cubical-type: (X)
, 
constant-presheaf-type: (X)
, 
I_cube: A(I)
, 
I_set: A(I)
, 
cube-set-restriction: f(s)
, 
psc-restriction: f(s)
Lemmas referenced : 
constant-presheaf-type_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{}[X:SmallCubicalSet].  \mforall{}[Gamma:j\mvdash{}].    Gamma  \mvdash{}  (X)
Date html generated:
2020_05_20-PM-02_32_49
Last ObjectModification:
2020_04_03-PM-08_43_10
Theory : cubical!type!theory
Home
Index