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:
2017_01_19-PM-02_53_35
Last ObjectModification:
2017_01_11-PM-10_13_16
Theory : small!categories
Home
Index