Nuprl Lemma : functor-cat_wf

[C1,C2:SmallCategory].  (FUN(C1;C2) ∈ SmallCategory)


Proof




Definitions occuring in Statement :  functor-cat: FUN(C1;C2) small-category: SmallCategory uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T functor-cat: FUN(C1;C2) small-category: SmallCategory subtype_rel: A ⊆B spreadn: spread4 and: P ∧ Q cand: c∧ B all: x:A. B[x] squash: T prop: nat-trans: nat-trans(C;D;F;G) 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 :  cat-functor_wf nat-trans_wf identity-trans_wf trans-comp_wf equal_wf squash_wf true_wf cat-arrow_wf functor-ob_wf nat-trans-equation cat-comp_wf functor-arrow_wf iff_weakening_equal cat-ob_wf trans-id-property all_wf trans-comp-assoc small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality dependent_pairEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality because_Cache independent_pairEquality applyEquality sqequalRule productEquality functionEquality functionExtensionality cumulativity universeEquality lambdaFormation imageElimination equalityTransitivity equalitySymmetry setElimination rename natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination dependent_functionElimination independent_pairFormation axiomEquality isect_memberEquality

Latex:
\mforall{}[C1,C2:SmallCategory].    (FUN(C1;C2)  \mmember{}  SmallCategory)



Date html generated: 2017_10_05-AM-00_46_22
Last ObjectModification: 2017_07_28-AM-09_19_26

Theory : small!categories


Home Index