### Nuprl Lemma : functor-comp-assoc

`∀[A,B,C,D:SmallCategory]. ∀[F:Functor(A;B)]. ∀[G:Functor(B;C)]. ∀[H:Functor(C;D)].`
`  (functor-comp(F;functor-comp(G;H)) = functor-comp(functor-comp(F;G);H) ∈ Functor(A;D))`

Proof

Definitions occuring in Statement :  functor-comp: `functor-comp(F;G)` cat-functor: `Functor(C1;C2)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` functor-comp: `functor-comp(F;G)` all: `∀x:A. B[x]` top: `Top` compose: `f o g`
Lemmas referenced :  equal-functors functor-comp_wf functor-ob_wf cat-ob_wf functor-arrow_wf cat-arrow_wf cat-functor_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination sqequalRule dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation applyEquality because_Cache axiomEquality

Latex:
\mforall{}[A,B,C,D:SmallCategory].  \mforall{}[F:Functor(A;B)].  \mforall{}[G:Functor(B;C)].  \mforall{}[H:Functor(C;D)].
(functor-comp(F;functor-comp(G;H))  =  functor-comp(functor-comp(F;G);H))

Date html generated: 2020_05_20-AM-07_53_31
Last ObjectModification: 2017_01_11-PM-10_13_16

Theory : small!categories

Home Index