Nuprl Lemma : op-op-cat

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


Proof




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

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



Date html generated: 2019_10_31-AM-07_24_06
Last ObjectModification: 2018_11_10-AM-11_32_30

Theory : small!categories


Home Index