Nuprl Lemma : cat_ob_op_lemma
∀C:SmallCategory. (cat-ob(op-cat(C)) ~ cat-ob(C))
Proof
Definitions occuring in Statement :
op-cat: op-cat(C),
cat-ob: cat-ob(C),
small-category: SmallCategory,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
member: t ∈ T,
all: ∀x:A. B[x],
pi1: fst(t),
spreadn: spread4,
op-cat: op-cat(C),
cat-ob: cat-ob(C),
small-category: SmallCategory
Lemmas referenced :
small-category_wf
Rules used in proof :
lemma_by_obid,
hypothesis,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
sqequalRule,
productElimination,
rename,
thin,
setElimination,
sqequalHypSubstitution
Latex:
\mforall{}C:SmallCategory. (cat-ob(op-cat(C)) \msim{} cat-ob(C))
Date html generated:
2016_05_18-AM-11_53_18
Last ObjectModification:
2015_12_28-PM-02_23_46
Theory : small!categories
Home
Index