---

Step * of Lemma id_prod_cat_lemma

∀x,B,A:Top.  (cat-id(A × B) x ~ <cat-id(A) (fst(x)), cat-id(B) (snd(x))>)
BY
{ (((UnivCD THENA Auto) THEN RepUR ``cat-id product-cat`` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,B,A:Top.    (cat-id(A  \mtimes{}  B)  x  \msim{}  <cat-id(A)  (fst(x)),  cat-id(B)  (snd(x))>)


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  RepUR  ``cat-id  product-cat``  0)  THEN  Auto)

---

Home Index