---

Step * of Lemma functor-arrow-prod-id

∀[A,B,C:SmallCategory]. ∀[F:Functor(A × B;C)]. ∀[a:cat-ob(A)]. ∀[b:cat-ob(B)].
  ((arrow(F) <a, b> <a, b> <cat-id(A) a, cat-id(B) b>) = (cat-id(C) (ob(F) <a, b>)) ∈ (cat-arrow(C) (ob(F) <a, b>) (ob(F\000C) <a, b>)))
BY
{ ((Auto THEN Subst' <cat-id(A) a, cat-id(B) b> ~ cat-id(A × B) <a, b> 0) THEN Auto) }

1
.....equality..... 
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. F : Functor(A × B;C)
5. a : cat-ob(A)
6. b : cat-ob(B)
⊢ <cat-id(A) a, cat-id(B) b> ~ cat-id(A × B) <a, b>

---

Latex:

---

Latex:
\mforall{}[A,B,C:SmallCategory].  \mforall{}[F:Functor(A  \mtimes{}  B;C)].  \mforall{}[a:cat-ob(A)].  \mforall{}[b:cat-ob(B)].
    ((arrow(F)  <a,  b>  <a,  b>  <cat-id(A)  a,  cat-id(B)  b>)  =  (cat-id(C)  (ob(F)  <a,  b>)))


By

---

Latex:
((Auto  THEN  Subst'  <cat-id(A)  a,  cat-id(B)  b>  \msim{}  cat-id(A  \mtimes{}  B)  <a,  b>  0)  THEN  Auto)

---

Home Index