Nuprl Lemma : small-category-subtype'
SmallCategory ⊆r small-category{i'':l}
Proof
Definitions occuring in Statement :
small-category: SmallCategory,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
subtype_rel: A ⊆r B,
member: t ∈ T
Lemmas referenced :
small-category-subtype,
small-category_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality,
cut,
hypothesisEquality,
applyEquality,
thin,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
sqequalRule,
instantiate
Latex:
SmallCategory \msubseteq{}r small-category\{i'':l\}
Date html generated:
2020_05_20-AM-07_49_25
Last ObjectModification:
2018_05_20-PM-10_08_11
Theory : small!categories
Home
Index