---

Step * 1 2 3 of Lemma poset-cat_wf

.....eq aux..... 
1. J : Cname List
2. arrow : name-morph(J;[]) ⟶ name-morph(J;[]) ⟶ Type
⊢ x:name-morph(J;[]) ⟶ (arrow x x) × (x:name-morph(J;[])
                                      ⟶ y:name-morph(J;[])
                                      ⟶ z:name-morph(J;[])
                                      ⟶ (arrow x y)
                                      ⟶ (arrow y z)
                                      ⟶ (arrow x z)) ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  J  :  Cname  List
2.  arrow  :  name-morph(J;[])  {}\mrightarrow{}  name-morph(J;[])  {}\mrightarrow{}  Type
\mvdash{}  x:name-morph(J;[])  {}\mrightarrow{}  (arrow  x  x)  \mtimes{}  (x:name-morph(J;[])
                                                                            {}\mrightarrow{}  y:name-morph(J;[])
                                                                            {}\mrightarrow{}  z:name-morph(J;[])
                                                                            {}\mrightarrow{}  (arrow  x  y)
                                                                            {}\mrightarrow{}  (arrow  y  z)
                                                                            {}\mrightarrow{}  (arrow  x  z))  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index