Nuprl Lemma : op-cat_wf

[C:SmallCategory]. (op-cat(C) ∈ SmallCategory)


Proof




Definitions occuring in Statement :  op-cat: op-cat(C) small-category: SmallCategory uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T op-cat: op-cat(C) small-category: SmallCategory spreadn: spread4 and: P ∧ Q subtype_rel: A ⊆B cand: c∧ B all: x:A. B[x] squash: T prop: true: True uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  equal_wf squash_wf true_wf iff_weakening_equal all_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution setElimination thin rename productElimination dependent_set_memberEquality dependent_pairEquality cumulativity hypothesisEquality lambdaEquality applyEquality functionExtensionality because_Cache independent_pairEquality hypothesis productEquality functionEquality universeEquality lambdaFormation independent_pairFormation imageElimination extract_by_obid isectElimination equalityTransitivity equalitySymmetry dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination independent_functionElimination axiomEquality

Latex:
\mforall{}[C:SmallCategory].  (op-cat(C)  \mmember{}  SmallCategory)



Date html generated: 2017_10_05-AM-00_46_25
Last ObjectModification: 2017_07_28-AM-09_19_28

Theory : small!categories


Home Index