Nuprl Lemma : trans-comp-assoc
∀C1,C2:SmallCategory. ∀x,y,z,w:Functor(C1;C2). ∀f:nat-trans(C1;C2;x;y). ∀g:nat-trans(C1;C2;y;z).
∀h:nat-trans(C1;C2;z;w).
(f o g o h = f o g o h ∈ nat-trans(C1;C2;x;w))
Proof
Definitions occuring in Statement :
trans-comp: t1 o t2,
nat-trans: nat-trans(C;D;F;G),
cat-functor: Functor(C1;C2),
small-category: SmallCategory,
all: ∀x:A. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
squash: ↓T,
uall: ∀[x:A]. B[x],
prop: ℙ,
subtype_rel: A ⊆r B,
nat-trans: nat-trans(C;D;F;G),
true: True,
uimplies: b supposing a,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
top: Top,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
equal_wf,
squash_wf,
true_wf,
cat-arrow_wf,
functor-ob_wf,
nat-trans-equation,
trans-comp_wf,
cat-comp_wf,
functor-arrow_wf,
nat-trans_wf,
iff_weakening_equal,
cat-ob_wf,
trans_comp_ap_lemma,
cat-comp-assoc,
all_wf,
cat-functor_wf,
small-category_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
applyEquality,
thin,
lambdaEquality,
sqequalHypSubstitution,
imageElimination,
introduction,
extract_by_obid,
isectElimination,
hypothesisEquality,
equalityTransitivity,
hypothesis,
equalitySymmetry,
universeEquality,
because_Cache,
setElimination,
rename,
sqequalRule,
natural_numberEquality,
imageMemberEquality,
baseClosed,
independent_isectElimination,
productElimination,
independent_functionElimination,
dependent_set_memberEquality,
functionExtensionality,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
\mforall{}C1,C2:SmallCategory. \mforall{}x,y,z,w:Functor(C1;C2). \mforall{}f:nat-trans(C1;C2;x;y). \mforall{}g:nat-trans(C1;C2;y;z).
\mforall{}h:nat-trans(C1;C2;z;w).
(f o g o h = f o g o h)
Date html generated:
2020_05_20-AM-07_51_45
Last ObjectModification:
2017_07_28-AM-09_19_22
Theory : small!categories
Home
Index