---

Step * 1 3 of Lemma poset-cat_wf

.....eq aux..... 
1. J : Cname List
2. 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))
  ∈ 𝕌'
BY
{ Auto }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  J  :  Cname  List
2.  ob  :  Type
\mvdash{}  arrow:ob  {}\mrightarrow{}  ob  {}\mrightarrow{}  Type
    \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))  \mmember{}  \mBbbU{}'


By

---

Latex:
Auto

---

Home Index