---

Step * of Lemma poset-functor_wf

∀[J,K:Cname List]. ∀[f:name-morph(J;K)].  (poset-functor(J;K;f) ∈ Functor(poset-cat(K);poset-cat(J)))
BY
{ (Auto
   THEN MemTypeCD
   THEN Try (Complete (Auto))
   THEN RepUR ``poset-cat cat-ob cat-arrow cat-id cat-comp poset-functor`` 0
   THEN Auto) }

1
1. J : Cname List
2. K : Cname List
3. f : name-morph(J;K)
4. g : name-morph(K;[])
5. h : name-morph(K;[])
6. p : ∀x@0:nameset(K). (↑g x@0 ≤z h x@0)
7. x : nameset(J)
⊢ ((f o g) x) ≤ ((f o h) x)

2
1. J : Cname List
2. K : Cname List
3. f : name-morph(J;K)
4. ∀x:name-morph(K;[]). ((λx.Ax) = (λx.Ax) ∈ (∀x@0:nameset(J). (↑(f o x) x@0 ≤z (f o x) x@0)))
5. x : name-morph(K;[])
6. y : name-morph(K;[])
7. z : name-morph(K;[])
8. f@0 : ∀x@0:nameset(K). (↑x x@0 ≤z y x@0)
9. g : ∀x:nameset(K). (↑y x ≤z z x)
10. x1 : nameset(J)
⊢ ((f o x) x1) ≤ ((f o z) x1)

---

Latex:

---

Latex:
\mforall{}[J,K:Cname  List].  \mforall{}[f:name-morph(J;K)].
    (poset-functor(J;K;f)  \mmember{}  Functor(poset-cat(K);poset-cat(J)))


By

---

Latex:
(Auto
  THEN  MemTypeCD
  THEN  Try  (Complete  (Auto))
  THEN  RepUR  ``poset-cat  cat-ob  cat-arrow  cat-id  cat-comp  poset-functor``  0
  THEN  Auto)

---

Home Index