---

Step * of 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>)))
BY
{ (Intros
   THEN (InstLemma `functor-arrow-comp` 
         [⌜A × B⌝;⌜C⌝;⌜F⌝;⌜<a1, b1>⌝;⌜<a2, b2>⌝;⌜<a3, b3>⌝;⌜<f, h>⌝;⌜<g, k>⌝]⋅
         THENA Auto
         )
   THEN Reduce -1
   THEN Trivial) }

---

Latex:

---

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>))


By

---

Latex:
(Intros
  THEN  (InstLemma  `functor-arrow-comp` 
              [\mkleeneopen{}A  \mtimes{}  B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}<a1,  b1>\mkleeneclose{};\mkleeneopen{}<a2,  b2>\mkleeneclose{};\mkleeneopen{}<a3,  b3>\mkleeneclose{};\mkleeneopen{}<f,  h>\mkleeneclose{};\mkleeneopen{}<g,  k>\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Reduce  -1
  THEN  Trivial)

---

Home Index