---

Step * of Lemma unique-poset-functor

∀C:SmallCategory. ∀I:Cname List. ∀L:name-morph(I;[]) ⟶ cat-ob(C). ∀E:i:nameset(I)
                                                                      ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} 
                                                                      ⟶ (cat-arrow(C) (L c) (L flip(c;i))).
  (edge-arrows-commute(C;I;L;E) ⇒ (∃!F:Functor(poset-cat(I);C). poset-functor-extends(C;I;L;E;F)))
BY
{ Auto }

1
1. C : SmallCategory@i'
2. I : Cname List@i
3. L : name-morph(I;[]) ⟶ cat-ob(C)@i
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2}  ⟶ (cat-arrow(C) (L c) (L flip(c;i)))@i
5. edge-arrows-commute(C;I;L;E)@i
⊢ ∃!F:Functor(poset-cat(I);C). poset-functor-extends(C;I;L;E;F)

---

Latex:

---

Latex:
\mforall{}C:SmallCategory.  \mforall{}I:Cname  List.  \mforall{}L:name-morph(I;[])  {}\mrightarrow{}  cat-ob(C).  \mforall{}E:i:nameset(I)
                                                                                                                                            {}\mrightarrow{}  c:\{c:name-morph(I;[])| 
                                                                                                                                                        (c  i)  =  0\} 
                                                                                                                                            {}\mrightarrow{}  (cat-arrow(C)  (L  c) 
                                                                                                                                                    (L  flip(c;i))).
    (edge-arrows-commute(C;I;L;E)  {}\mRightarrow{}  (\mexists{}!F:Functor(poset-cat(I);C).  poset-functor-extends(C;I;L;E;F)))


By

---

Latex:
Auto

---

Home Index