Nuprl Lemma : csm-subset-codomain

[X,Y,Z:j⊢].  j⟶ Y ⊆j⟶ supposing sub_cubical_set{j:l}(Y; Z)


Proof




Definitions occuring in Statement :  sub_cubical_set: Y ⊆ X cube_set_map: A ⟶ B cubical_set: CubicalSet uimplies: supposing a subtype_rel: A ⊆B 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)
Lemmas referenced :  pscm-subset-codomain cube-cat_wf
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesis sqequalRule

Latex:
\mforall{}[X,Y,Z:j\mvdash{}].    X  j{}\mrightarrow{}  Y  \msubseteq{}r  X  j{}\mrightarrow{}  Z  supposing  sub\_cubical\_set\{j:l\}(Y;  Z)



Date html generated: 2020_05_20-PM-02_33_52
Last ObjectModification: 2020_04_03-PM-08_44_19

Theory : cubical!type!theory


Home Index