---

Step * of Lemma cat-cat_wf

Cat ∈ SmallCategory'
BY
{ At ⌜𝕌'⌝ MemTypeCD⋅ }

1
Cat ∈ ob:𝕌'
× arrow:ob ⟶ ob ⟶ 𝕌'
× x:ob ⟶ (arrow x x)
× (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z))

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

3
.....wf..... 
1. cat : ob:𝕌'
× arrow:ob ⟶ ob ⟶ 𝕌'
× x:ob ⟶ (arrow x x)
× (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z))
⊢ istype(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:
Cat  \mmember{}  SmallCategory'


By

---

Latex:
At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  MemTypeCD\mcdot{}

---

Home Index