---

Step * 1 of Lemma poset-functor-comp


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))
BY
{ (RepUR ``poset-functor functor-comp`` 0 THEN RepUR ``poset-cat`` -1 THEN RepUR ``poset-cat`` 0) }

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 : name-morph(K;[])
⊢ ((f o g) o x) = (f o (g o x)) ∈ name-morph(I;[])

---

Latex:

---

Latex:

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))
\mvdash{}  (ob(poset-functor(I;K;(f  o  g)))  x)
=  (ob(functor-comp(poset-functor(J;K;g);poset-functor(I;J;f)))  x)


By

---

Latex:
(RepUR  ``poset-functor  functor-comp``  0  THEN  RepUR  ``poset-cat``  -1  THEN  RepUR  ``poset-cat``  0)

---

Home Index