---

Step * 1 of Lemma poset-cat_wf


1. J : Cname List
⊢ <name-morph(J;[]), λf,g. ∀x:nameset(J). (↑f x ≤z g x), λf,x. Ax, λf,g,h,p,q,x. Ax> ∈ 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
{ MemCD }

1
.....subterm..... T:t
1:n
1. J : Cname List
⊢ name-morph(J;[]) ∈ Type

2
.....subterm..... T:t
2:n
1. J : Cname List
⊢ <λf,g. ∀x:nameset(J). (↑f x ≤z g x), λf,x. Ax, λf,g,h,p,q,x. Ax> ∈ 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))

3
.....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))
  ∈ 𝕌'

---

Latex:

---

Latex:

1.  J  :  Cname  List
\mvdash{}  <name-morph(J;[]),  \mlambda{}f,g.  \mforall{}x:nameset(J).  (\muparrow{}f  x  \mleq{}z  g  x),  \mlambda{}f,x.  Ax,  \mlambda{}f,g,h,p,q,x.  Ax>  \mmember{}  ob:Type
    \mtimes{}  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))


By

---

Latex:
MemCD

---

Home Index