Nuprl Lemma : unit-cat_wf
1 ∈ SmallCategory
Proof
Definitions occuring in Statement :
unit-cat: 1,
small-category: SmallCategory,
member: t ∈ T
Definitions unfolded in proof :
unit-cat: 1,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
discrete-cat_wf,
unit_wf2
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis
Latex:
1 \mmember{} SmallCategory
Date html generated:
2017_01_19-PM-02_51_56
Last ObjectModification:
2017_01_13-PM-04_05_31
Theory : small!categories
Home
Index