### Nuprl Lemma : functor-arrow-comp

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

Proof

Definitions occuring in Statement :  functor-arrow: `functor-arrow(F)` functor-ob: `functor-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: `f a` equal: `s = t ∈ T`
Definitions unfolded in proof :  top: `Top` all: `∀x:A. B[x]` mk-functor: `mk-functor(ob;arrow)` and: `P ∧ Q` cat-functor: `Functor(C1;C2)` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  small-category_wf cat-functor_wf cat-ob_wf cat-arrow_wf functor_arrow_pair_lemma functor_ob_pair_lemma
Rules used in proof :  because_Cache axiomEquality isectElimination applyEquality hypothesisEquality hypothesis voidEquality voidElimination isect_memberEquality dependent_functionElimination extract_by_obid sqequalRule productElimination rename thin setElimination sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

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].
((functor-arrow(F)  x  z  (cat-comp(C)  x  y  z  f  g))
=  (cat-comp(D)  (functor-ob(F)  x)  (functor-ob(F)  y)  (functor-ob(F)  z)  (functor-arrow(F)  x  y  f)
(functor-arrow(F)  y  z  g)))

Date html generated: 2017_01_11-AM-09_17_59
Last ObjectModification: 2017_01_10-PM-00_33_29

Theory : small!categories

Home Index