Nuprl Lemma : pscm-subset-subtype
∀[C:SmallCategory]. ∀[A,B,Y,Z:ps_context{j:l}(C)].
  (psc_map{j:l}(C; Y; A) ⊆r psc_map{j:l}(C; Z; B)) supposing 
     (sub_ps_context{j:l}(C; A; B) and 
     sub_ps_context{j:l}(C; Z; Y))
Proof
Definitions occuring in Statement : 
sub_ps_context: Y ⊆ X
, 
psc_map: A ⟶ B
, 
ps_context: __⊢
, 
uimplies: b supposing a
, 
subtype_rel: A ⊆r B
, 
uall: ∀[x:A]. B[x]
, 
small-category: SmallCategory
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
uimplies: b supposing a
, 
and: P ∧ Q
, 
cand: A c∧ B
, 
member: t ∈ T
, 
guard: {T}
, 
subtype_rel: A ⊆r B
Lemmas referenced : 
psc_map_subtype3, 
sub_ps_context_self, 
subtype_rel_transitivity, 
psc_map_wf, 
sub_ps_context_wf, 
ps_context_wf, 
small-category-cumulativity-2, 
small-category_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
cut, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
because_Cache, 
independent_isectElimination, 
hypothesis, 
independent_pairFormation, 
productElimination, 
instantiate, 
applyEquality, 
sqequalRule, 
universeIsType
Latex:
\mforall{}[C:SmallCategory].  \mforall{}[A,B,Y,Z:ps\_context\{j:l\}(C)].
    (psc\_map\{j:l\}(C;  Y;  A)  \msubseteq{}r  psc\_map\{j:l\}(C;  Z;  B))  supposing 
          (sub\_ps\_context\{j:l\}(C;  A;  B)  and 
          sub\_ps\_context\{j:l\}(C;  Z;  Y))
Date html generated:
2020_05_20-PM-01_35_23
Last ObjectModification:
2020_04_02-PM-06_35_23
Theory : presheaf!models!of!type!theory
Home
Index