Nuprl Lemma : functor-arrow-comp

[C,D:SmallCategory]. ∀[F:Functor(C;D)]. ∀[x,y,z:cat-ob(C)]. ∀[f:cat-arrow(C) y]. ∀[g:cat-arrow(C) z].
  ((F (cat-comp(C) g)) (cat-comp(D) (F x) (F y) (F z) (F f) (F g)) ∈ (cat-arrow(D) (F x) (F z)))


Proof




Definitions occuring in Statement :  functor-arrow: arrow(F) functor-ob: ob(F) cat-functor: Functor(C1;C2) cat-comp: cat-comp(C) cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) small-category: SmallCategory uall: [x:A]. B[x] apply: a equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] cat-functor: Functor(C1;C2) and: P ∧ Q all: x:A. B[x] member: t ∈ T
Lemmas referenced :  ob_pair_lemma arrow_pair_lemma cat-arrow_wf cat-ob_wf cat-functor_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut sqequalHypSubstitution setElimination thin rename productElimination sqequalRule introduction extract_by_obid dependent_functionElimination Error :memTop,  hypothesis hypothesisEquality universeIsType applyEquality isectElimination because_Cache inhabitedIsType

Latex:
\mforall{}[C,D:SmallCategory].  \mforall{}[F:Functor(C;D)].  \mforall{}[x,y,z:cat-ob(C)].  \mforall{}[f:cat-arrow(C)  x  y].
\mforall{}[g:cat-arrow(C)  y  z].
    ((F  x  z  (cat-comp(C)  x  y  z  f  g))  =  (cat-comp(D)  (F  x)  (F  y)  (F  z)  (F  x  y  f)  (F  y  z  g)))



Date html generated: 2020_05_20-AM-07_51_05
Last ObjectModification: 2019_12_30-PM-02_10_27

Theory : small!categories


Home Index