Nuprl Lemma : equal-functors

[A,B:SmallCategory]. ∀[F,G:Functor(A;B)].
  (F G ∈ Functor(A;B)) supposing 
     ((∀x,y:cat-ob(A). ∀f:cat-arrow(A) y.
         ((arrow(F) f) (arrow(G) f) ∈ (cat-arrow(B) (ob(F) x) (ob(F) y)))) and 
     (∀x:cat-ob(A). ((ob(F) x) (ob(G) x) ∈ cat-ob(B))))


Definitions occuring in Statement :  functor-arrow: arrow(F) functor-ob: ob(F) cat-functor: Functor(C1;C2) cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) small-category: SmallCategory uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] apply: a equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a cat-functor: Functor(C1;C2) and: P ∧ Q all: x:A. B[x] top: Top squash: T true: True subtype_rel: A ⊆B prop: guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q cand: c∧ B so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  ob_pair_lemma arrow_pair_lemma equal_wf cat-ob_wf iff_weakening_equal cat-arrow_wf all_wf cat-id_wf cat-comp_wf functor-ob_wf functor-arrow_wf subtype_rel-equal squash_wf true_wf cat-functor_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename productElimination sqequalRule extract_by_obid dependent_functionElimination isect_memberEquality voidElimination voidEquality hypothesis dependent_set_memberEquality dependent_pairEquality functionExtensionality applyEquality lambdaEquality imageElimination isectElimination because_Cache hypothesisEquality natural_numberEquality imageMemberEquality baseClosed universeEquality equalityTransitivity equalitySymmetry independent_isectElimination independent_functionElimination functionEquality independent_pairFormation productEquality instantiate axiomEquality

\mforall{}[A,B:SmallCategory].  \mforall{}[F,G:Functor(A;B)].
    (F  =  G)  supposing 
          ((\mforall{}x,y:cat-ob(A).  \mforall{}f:cat-arrow(A)  x  y.    ((arrow(F)  x  y  f)  =  (arrow(G)  x  y  f)))  and 
          (\mforall{}x:cat-ob(A).  ((ob(F)  x)  =  (ob(G)  x))))

Date html generated: 2017_10_05-AM-00_47_26
Last ObjectModification: 2017_07_28-AM-09_19_41

Theory : small!categories

Home Index