---

Step * 1 2 of Lemma poset-cat_wf

.....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))
BY
{ (MemCD THEN Reduce 0) }

1
.....subterm..... T:t
1:n
1. J : Cname List
⊢ λf,g. ∀x:nameset(J). (↑f x ≤z g x) ∈ name-morph(J;[]) ⟶ name-morph(J;[]) ⟶ Type

2
1. J : Cname List
⊢ <λf,x. Ax, λf,g,h,p,q,x. Ax> ∈ x:name-morph(J;[]) ⟶ (∀x@0:nameset(J). (↑x x@0 ≤z x x@0)) × (x:name-morph(J;[])
                                                                              ⟶ y:name-morph(J;[])
                                                                              ⟶ z:name-morph(J;[])
                                                                              ⟶ (∀x@0:nameset(J). (↑x x@0 ≤z y x@0))
                                                                              ⟶ (∀x:nameset(J). (↑y x ≤z z x))
                                                                              ⟶ (∀x@0:nameset(J). (↑x x@0 ≤z z x@0)))

3
.....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

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  J  :  Cname  List
\mvdash{}  <\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{}  arrow:name-morph(J;[])  {}\mrightarrow{}  name-\000Cmorph(J;[])  {}\mrightarrow{}  Type
    \mtimes{}  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))


By

---

Latex:
(MemCD  THEN  Reduce  0)

---

Home Index