---

Step * of Lemma product-cat_wf

∀[A,B:SmallCategory].  (A × B ∈ SmallCategory)
BY
{ (Intros THEN At ⌜𝕌'⌝MemTypeCD⋅) }

1
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))

2
.....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)))  

3
.....wf..... 
1. A : SmallCategory
2. B : SmallCategory
3. cat : 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))
⊢ let ob,arrow,id,comp = cat 
  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)))   ∈ 𝕌'

---

Latex:

---

Latex:
\mforall{}[A,B:SmallCategory].    (A  \mtimes{}  B  \mmember{}  SmallCategory)


By

---

Latex:
(Intros  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}MemTypeCD\mcdot{})

---

Home Index