---

Step * of Lemma poset_functor_extend-is-functor

No Annotations
∀[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)))].
  <L, λc1,c2,p. poset_functor_extend(C;I;L;E;c1;c2)> ∈ Functor(poset-cat(I);C) supposing edge-arrows-commute(C;I;L;E)
BY
{ ((UnivCD THENA Auto) THEN MemTypeCD THEN Reduce 0 THEN 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. edge-arrows-commute(C;I;L;E)
6. c1 : cat-ob(poset-cat(I))
7. c2 : cat-ob(poset-cat(I))
8. p : cat-arrow(poset-cat(I)) c1 c2
9. x : nameset(I)
⊢ (c1 x) ≤ (c2 x)

2
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. edge-arrows-commute(C;I;L;E)
6. ∀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)))
7. x : cat-ob(poset-cat(I))
8. y : cat-ob(poset-cat(I))
9. z : cat-ob(poset-cat(I))
10. f : cat-arrow(poset-cat(I)) x y
11. g : cat-arrow(poset-cat(I)) y z
⊢ poset_functor_extend(C;I;L;E;x;z)
= (cat-comp(C) (L x) (L y) (L z) poset_functor_extend(C;I;L;E;x;y) poset_functor_extend(C;I;L;E;y;z))
∈ (cat-arrow(C) (L x) (L z))

---

Latex:

---

Latex:
No  Annotations
\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)))].
    <L,  \mlambda{}c1,c2,p.  poset\_functor\_extend(C;I;L;E;c1;c2)>  \mmember{}  Functor(poset-cat(I);C) 
    supposing  edge-arrows-commute(C;I;L;E)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index