---

Step * 3 of Lemma cat-cat_wf

.....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)))  )
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  cat  :  ob:\mBbbU{}'
\mtimes{}  arrow:ob  {}\mrightarrow{}  ob  {}\mrightarrow{}  \mBbbU{}'
\mtimes{}  x:ob  {}\mrightarrow{}  (arrow  x  x)
\mtimes{}  (x:ob  {}\mrightarrow{}  y:ob  {}\mrightarrow{}  z:ob  {}\mrightarrow{}  (arrow  x  y)  {}\mrightarrow{}  (arrow  y  z)  {}\mrightarrow{}  (arrow  x  z))
\mvdash{}  istype(let  ob,arrow,id,comp  =  cat 
                  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:
Auto

---

Home Index