---

Step * 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. F : Functor(poset-cat(I);C)
6. ob(F) = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
⊢ ∀i:nameset(I). ∀c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} .
    ((F c flip(c;i) (λx.Ax)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i)))) ∈ Type
BY
{ ((RepeatFor 3 (MemCD) THEN Try (QuickAuto))
   THEN RepeatFor 2 (DVar `F')
   THEN RepUR ``functor-arrow`` 0
   THEN RepUR ``cat-ob poset-cat cat-arrow`` -5
   THEN Fold `cat-arrow` (-5)) }

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. 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} 
⊢ F2 c flip(c;i) (λx.Ax) ∈ cat-arrow(C) (L c) (L flip(c;i))

---

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.  F  :  Functor(poset-cat(I);C)
6.  ob(F)  =  L
\mvdash{}  \mforall{}i:nameset(I).  \mforall{}c:\{c:name-morph(I;[])|  (c  i)  =  0\}  .    ((F  c  flip(c;i)  (\mlambda{}x.Ax))  =  (E  i  c))  \mmember{}  Type


By

---

Latex:
((RepeatFor  3  (MemCD)  THEN  Try  (QuickAuto))
  THEN  RepeatFor  2  (DVar  `F')
  THEN  RepUR  ``functor-arrow``  0
  THEN  RepUR  ``cat-ob  poset-cat  cat-arrow``  -5
  THEN  Fold  `cat-arrow`  (-5))

---

Home Index