Nuprl Lemma : sub_cubical_set_functionality
∀[Y,X:j⊢]. ∀[A:{X ⊢ _}].  sub_cubical_set{[i | j]:l}(Y.A; X.A) supposing sub_cubical_set{j:l}(Y; X)
Proof
Definitions occuring in Statement : 
cube-context-adjoin: X.A
, 
cubical-type: {X ⊢ _}
, 
sub_cubical_set: Y ⊆ X
, 
cubical_set: CubicalSet
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
cubical_set: CubicalSet
, 
sub_cubical_set: Y ⊆ X
, 
sub_ps_context: Y ⊆ X
, 
cube_set_map: A ⟶ B
, 
csm-id: 1(X)
, 
pscm-id: 1(X)
, 
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)
Lemmas referenced : 
sub_ps_context_functionality, 
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{}[Y,X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].    sub\_cubical\_set\{[i  |  j]:l\}(Y.A;  X.A)  supposing  sub\_cubical\_set\{j:l\}(Y;  X)
Date html generated:
2020_05_20-PM-02_34_21
Last ObjectModification:
2020_04_04-AM-09_22_18
Theory : cubical!type!theory
Home
Index