---

Step * 1 of Lemma product-cat_wf


1. A : SmallCategory
2. B : SmallCategory
⊢ A × B ∈ ob:Type
  × arrow:ob ⟶ ob ⟶ Type
  × x:ob ⟶ (arrow x x)
  × (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z))
BY
{ (RepUR ``product-cat`` 0 THEN (MemCD THENL [Auto; Reduce 0; Auto])) }

1
.....subterm..... T:t
2:n
1. A : SmallCategory
2. B : SmallCategory
⊢ <λxy,uv. (cat-arrow(A) (fst(xy)) (fst(uv)) × (cat-arrow(B) (snd(xy)) (snd(uv))))
  , λxy.<cat-id(A) (fst(xy)), cat-id(B) (snd(xy))>
  , λxy,uv,wz,F,G. <cat-comp(A) (fst(xy)) (fst(uv)) (fst(wz)) (fst(F)) (fst(G))
                   , cat-comp(B) (snd(xy)) (snd(uv)) (snd(wz)) (snd(F)) (snd(G))
                   >> ∈ 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))

---

Latex:

---

Latex:

1.  A  :  SmallCategory
2.  B  :  SmallCategory
\mvdash{}  A  \mtimes{}  B  \mmember{}  ob:Type
    \mtimes{}  arrow:ob  {}\mrightarrow{}  ob  {}\mrightarrow{}  Type
    \mtimes{}  x:ob  {}\mrightarrow{}  (arrow  x  x)
    \mtimes{}  (x:ob  {}\mrightarrow{}  y:ob  {}\mrightarrow{}  z:ob  {}\mrightarrow{}  (arrow  x  y)  {}\mrightarrow{}  (arrow  y  z)  {}\mrightarrow{}  (arrow  x  z))


By

---

Latex:
(RepUR  ``product-cat``  0  THEN  (MemCD  THENL  [Auto;  Reduce  0;  Auto]))

---

Home Index