---

Step * of Lemma poset_functor_extend_id

∀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))).
∀x:cat-ob(poset-cat(I)).
  (poset_functor_extend(C;I;L;E;x;x) = (cat-id(C) (L x)) ∈ (cat-arrow(C) (L x) (L x)))
BY
{ Auto }

1
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. x : cat-ob(poset-cat(I))
⊢ poset_functor_extend(C;I;L;E;x;x) = (cat-id(C) (L x)) ∈ (cat-arrow(C) (L x) (L x))

---

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))).
\mforall{}x:cat-ob(poset-cat(I)).
    (poset\_functor\_extend(C;I;L;E;x;x)  =  (cat-id(C)  (L  x)))


By

---

Latex:
Auto

---

Home Index