---

Step * 1 1 3 of Lemma product-cat_wf

.....eq aux..... 
1. A : SmallCategory
2. B : SmallCategory
3. arrow : (cat-ob(A) × cat-ob(B)) ⟶ (cat-ob(A) × cat-ob(B)) ⟶ Type
⊢ x:(cat-ob(A) × cat-ob(B)) ⟶ (arrow x x) × (x:(cat-ob(A) × cat-ob(B))
                                             ⟶ y:(cat-ob(A) × cat-ob(B))
                                             ⟶ z:(cat-ob(A) × cat-ob(B))
                                             ⟶ (arrow x y)
                                             ⟶ (arrow y z)
                                             ⟶ (arrow x z)) ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  A  :  SmallCategory
2.  B  :  SmallCategory
3.  arrow  :  (cat-ob(A)  \mtimes{}  cat-ob(B))  {}\mrightarrow{}  (cat-ob(A)  \mtimes{}  cat-ob(B))  {}\mrightarrow{}  Type
\mvdash{}  x:(cat-ob(A)  \mtimes{}  cat-ob(B))  {}\mrightarrow{}  (arrow  x  x)  \mtimes{}  (x:(cat-ob(A)  \mtimes{}  cat-ob(B))
                                                                                          {}\mrightarrow{}  y:(cat-ob(A)  \mtimes{}  cat-ob(B))
                                                                                          {}\mrightarrow{}  z:(cat-ob(A)  \mtimes{}  cat-ob(B))
                                                                                          {}\mrightarrow{}  (arrow  x  y)
                                                                                          {}\mrightarrow{}  (arrow  y  z)
                                                                                          {}\mrightarrow{}  (arrow  x  z))  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index