---

Step * 1 1 1 of Lemma product-cat_wf

.....subterm..... T:t
1:n
1. A : SmallCategory
2. B : SmallCategory
⊢ λxy,uv. (cat-arrow(A) (fst(xy)) (fst(uv)) × (cat-arrow(B) (snd(xy)) (snd(uv)))) ∈ (cat-ob(A) × cat-ob(B))
  ⟶ (cat-ob(A) × cat-ob(B))
  ⟶ Type
BY
{ (RepeatFor 2 ((MemCD THENL [(D -1 THEN Reduce 0); Auto])) THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  SmallCategory
2.  B  :  SmallCategory
\mvdash{}  \mlambda{}xy,uv.  (cat-arrow(A)  (fst(xy))  (fst(uv))  \mtimes{}  (cat-arrow(B)  (snd(xy))  (snd(uv))))
    \mmember{}  (cat-ob(A)  \mtimes{}  cat-ob(B))  {}\mrightarrow{}  (cat-ob(A)  \mtimes{}  cat-ob(B))  {}\mrightarrow{}  Type


By

---

Latex:
(RepeatFor  2  ((MemCD  THENL  [(D  -1  THEN  Reduce  0);  Auto]))  THEN  Auto)

---

Home Index