---

Step * 2 of Lemma product-cat_wf

.....set predicate..... 
1. A : SmallCategory
2. B : SmallCategory
⊢ let ob,arrow,id,comp = A × B 
  in (∀x,y:ob. ∀f:arrow x y.  (((comp x x y (id x) f) = f ∈ (arrow x y)) ∧ ((comp x y y f (id y)) = f ∈ (arrow x y))))
     ∧ (∀x,y,z,w:ob. ∀f:arrow x y. ∀g:arrow y z. ∀h:arrow z w.
          ((comp x z w (comp x y z f g) h) = (comp x y w f (comp y z w g h)) ∈ (arrow x w)))  
BY
{ (RepUR ``product-cat`` 0
   THEN D 0
   THEN RepeatFor 3 (((D 0 THENA Auto) THEN D -1 THEN Reduce 0))
   THEN Auto
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  A  :  SmallCategory
2.  B  :  SmallCategory
\mvdash{}  let  ob,arrow,id,comp  =  A  \mtimes{}  B 
    in  (\mforall{}x,y:ob.  \mforall{}f:arrow  x  y.    (((comp  x  x  y  (id  x)  f)  =  f)  \mwedge{}  ((comp  x  y  y  f  (id  y))  =  f)))
          \mwedge{}  (\mforall{}x,y,z,w:ob.  \mforall{}f:arrow  x  y.  \mforall{}g:arrow  y  z.  \mforall{}h:arrow  z  w.
                    ((comp  x  z  w  (comp  x  y  z  f  g)  h)  =  (comp  x  y  w  f  (comp  y  z  w  g  h))))   


By

---

Latex:
(RepUR  ``product-cat``  0
  THEN  D  0
  THEN  RepeatFor  3  (((D  0  THENA  Auto)  THEN  D  -1  THEN  Reduce  0))
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index