---

Step * of Lemma poset-functor-comp

∀[I,J,K:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:name-morph(J;K)].
  (poset-functor(I;K;(f o g))
  = functor-comp(poset-functor(J;K;g);poset-functor(I;J;f))
  ∈ Functor(poset-cat(K);poset-cat(I)))
BY
{ (Auto THEN BLemma `equal-functors` THEN Auto) }

1
1. I : Cname List
2. J : Cname List
3. K : Cname List
4. f : name-morph(I;J)
5. g : name-morph(J;K)
6. x : cat-ob(poset-cat(K))
⊢ (ob(poset-functor(I;K;(f o g))) x)
= (ob(functor-comp(poset-functor(J;K;g);poset-functor(I;J;f))) x)
∈ cat-ob(poset-cat(I))

---

Latex:

---

Latex:
\mforall{}[I,J,K:Cname  List].  \mforall{}[f:name-morph(I;J)].  \mforall{}[g:name-morph(J;K)].
    (poset-functor(I;K;(f  o  g))  =  functor-comp(poset-functor(J;K;g);poset-functor(I;J;f)))


By

---

Latex:
(Auto  THEN  BLemma  `equal-functors`  THEN  Auto)

---

Home Index