Nuprl Lemma : functor-arrow-prod-comp
∀[A,B,C:SmallCategory]. ∀[F:Functor(A × B;C)]. ∀[a1,a2,a3:cat-ob(A)]. ∀[f:cat-arrow(A) a1 a2]. ∀[g:cat-arrow(A) a2 a3].
∀[b1,b2,b3:cat-ob(B)]. ∀[h:cat-arrow(B) b1 b2]. ∀[k:cat-arrow(B) b2 b3].
((cat-comp(C) (ob(F) <a1, b1>) (ob(F) <a2, b2>) (ob(F) <a3, b3>) (arrow(F) <a1, b1> <a2, b2> <f, h>) (arrow(F) <a2, b2\000C> <a3, b3> <g, k>))
= (arrow(F) <a1, b1> <a3, b3> <cat-comp(A) a1 a2 a3 f g, cat-comp(B) b1 b2 b3 h k>)
∈ (cat-arrow(C) (ob(F) <a1, b1>) (ob(F) <a3, b3>)))
Proof
Definitions occuring in Statement :
product-cat: A × B,
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: f a,
pair: <a, b>,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
top: Top,
subtype_rel: A ⊆r B,
pi1: fst(t),
pi2: snd(t)
Lemmas referenced :
functor-arrow-comp,
product-cat_wf,
ob_product_lemma,
arrow_prod_lemma,
cat-arrow_wf,
comp_product_cat_lemma,
cat-ob_wf,
cat-functor_wf,
small-category_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
sqequalRule,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality,
independent_pairEquality,
because_Cache,
applyEquality,
lambdaEquality,
productEquality,
equalitySymmetry
Latex:
\mforall{}[A,B,C:SmallCategory]. \mforall{}[F:Functor(A \mtimes{} B;C)]. \mforall{}[a1,a2,a3:cat-ob(A)]. \mforall{}[f:cat-arrow(A) a1 a2].
\mforall{}[g:cat-arrow(A) a2 a3]. \mforall{}[b1,b2,b3:cat-ob(B)]. \mforall{}[h:cat-arrow(B) b1 b2]. \mforall{}[k:cat-arrow(B) b2 b3].
((cat-comp(C) (ob(F) <a1, b1>) (ob(F) <a2, b2>) (ob(F) <a3, b3>) (arrow(F) <a1, b1> <a2, b2> <f, h\000C>) (arrow(F) <a2, b2> <a3, b3> <g, k>))
= (arrow(F) <a1, b1> <a3, b3> <cat-comp(A) a1 a2 a3 f g, cat-comp(B) b1 b2 b3 h k>))
Date html generated:
2017_01_19-PM-02_54_12
Last ObjectModification:
2017_01_11-PM-03_20_05
Theory : small!categories
Home
Index