---

Step * 2 1 2 of Lemma poset-functor-extends_wf


1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) ⟶ cat-ob(C)
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2}  ⟶ (cat-arrow(C) (L c) (L flip(c;i)))
5. F1 : cat-ob(poset-cat(I)) ⟶ cat-ob(C)
6. F2 : x:name-morph(I;[]) ⟶ y:name-morph(I;[]) ⟶ (∀x@0:nameset(I). (↑x x@0 ≤z y x@0)) ⟶ (cat-arrow(C) (F1 x) (F1 y))
7. let F,M = <F1, F2> 
   in (∀x:cat-ob(poset-cat(I)). ((M x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F x)) ∈ (cat-arrow(C) (F x) (F x))))
      ∧ (∀x,y,z:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) x y. ∀g:cat-arrow(poset-cat(I)) y z.
           ((M x z (cat-comp(poset-cat(I)) x y z f g))
           = (cat-comp(C) (F x) (F y) (F z) (M x y f) (M y z g))
           ∈ (cat-arrow(C) (F x) (F z))))
8. ob(<F1, F2>) = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
9. i : nameset(I)
10. c : {c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} 
11. (F2 c flip(c;i) (λx.Ax)) = (F2 c flip(c;i) (λx.Ax)) ∈ (cat-arrow(C) (F1 c) (F1 flip(c;i)))
⊢ (cat-arrow(C) (F1 c) (F1 flip(c;i))) ⊆r (cat-arrow(C) (L c) (L flip(c;i)))
BY
{ (RepUR ``functor-ob`` -4 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  I  :  Cname  List
3.  L  :  name-morph(I;[])  {}\mrightarrow{}  cat-ob(C)
4.  E  :  i:nameset(I)  {}\mrightarrow{}  c:\{c:name-morph(I;[])|  (c  i)  =  0\}    {}\mrightarrow{}  (cat-arrow(C)  (L  c)  (L  flip(c;i)))
5.  F1  :  cat-ob(poset-cat(I))  {}\mrightarrow{}  cat-ob(C)
6.  F2  :  x:name-morph(I;[])
{}\mrightarrow{}  y:name-morph(I;[])
{}\mrightarrow{}  (\mforall{}x@0:nameset(I).  (\muparrow{}x  x@0  \mleq{}z  y  x@0))
{}\mrightarrow{}  (cat-arrow(C)  (F1  x)  (F1  y))
7.  let  F,M  =  <F1,  F2> 
      in  (\mforall{}x:cat-ob(poset-cat(I)).  ((M  x  x  (cat-id(poset-cat(I))  x))  =  (cat-id(C)  (F  x))))
            \mwedge{}  (\mforall{}x,y,z:cat-ob(poset-cat(I)).  \mforall{}f:cat-arrow(poset-cat(I))  x  y.
                  \mforall{}g:cat-arrow(poset-cat(I))  y  z.
                      ((M  x  z  (cat-comp(poset-cat(I))  x  y  z  f  g))
                      =  (cat-comp(C)  (F  x)  (F  y)  (F  z)  (M  x  y  f)  (M  y  z  g))))
8.  ob(<F1,  F2>)  =  L
9.  i  :  nameset(I)
10.  c  :  \{c:name-morph(I;[])|  (c  i)  =  0\} 
11.  (F2  c  flip(c;i)  (\mlambda{}x.Ax))  =  (F2  c  flip(c;i)  (\mlambda{}x.Ax))
\mvdash{}  (cat-arrow(C)  (F1  c)  (F1  flip(c;i)))  \msubseteq{}r  (cat-arrow(C)  (L  c)  (L  flip(c;i)))


By

---

Latex:
(RepUR  ``functor-ob``  -4  THEN  Auto)

---

Home Index