---

Step * 1 of Lemma functor-arrow-prod-id

.....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>
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  A  :  SmallCategory
2.  B  :  SmallCategory
3.  C  :  SmallCategory
4.  F  :  Functor(A  \mtimes{}  B;C)
5.  a  :  cat-ob(A)
6.  b  :  cat-ob(B)
\mvdash{}  <cat-id(A)  a,  cat-id(B)  b>  \msim{}  cat-id(A  \mtimes{}  B)  <a,  b>


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index