---

Step * of Lemma poset-extend-unique

∀[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)))].
∀[F,G:Functor(poset-cat(I);C)].
  (F = G ∈ Functor(poset-cat(I);C)) supposing (poset-functor-extends(C;I;L;E;G) and poset-functor-extends(C;I;L;E;F))
BY
{ (Auto
   THEN DVar `F'
   THEN EqTypeCD
   THEN Auto
   THEN DVar `F'
   THEN RepeatFor 2 (DVar `G')
   THEN All (RepUR ``poset-functor-extends functor-ob functor-arrow``)
   THEN EqCD
   THEN Auto
   THEN RepeatFor 3 ((FunExt THENA 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. F1 : cat-ob(poset-cat(I)) ⟶ cat-ob(C)
6. F2 : x:cat-ob(poset-cat(I))
⟶ y:cat-ob(poset-cat(I))
⟶ (cat-arrow(poset-cat(I)) x y)
⟶ (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. F : cat-ob(poset-cat(I)) ⟶ cat-ob(C)
9. G1 : x:cat-ob(poset-cat(I)) ⟶ y:cat-ob(poset-cat(I)) ⟶ (cat-arrow(poset-cat(I)) x y) ⟶ (cat-arrow(C) (F x) (F y))
10. let F,M = <F, G1> 
    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))))
11. F1 = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
12. ∀i:nameset(I). ∀c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} .
      ((F2 c flip(c;i) (λx.Ax)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i))))
13. F = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
14. ∀i:nameset(I). ∀c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} .
      ((G1 c flip(c;i) (λx.Ax)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i))))
15. x : cat-ob(poset-cat(I))
16. y : cat-ob(poset-cat(I))
17. x1 : cat-arrow(poset-cat(I)) x y
⊢ (F2 x y x1) = (G1 x y x1) ∈ (cat-arrow(C) (F1 x) (F1 y))

---

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{}[F,G:Functor(poset-cat(I);C)].
    (F  =  G)  supposing  (poset-functor-extends(C;I;L;E;G)  and  poset-functor-extends(C;I;L;E;F))


By

---

Latex:
(Auto
  THEN  DVar  `F'
  THEN  EqTypeCD
  THEN  Auto
  THEN  DVar  `F'
  THEN  RepeatFor  2  (DVar  `G')
  THEN  All  (RepUR  ``poset-functor-extends  functor-ob  functor-arrow``)
  THEN  EqCD
  THEN  Auto
  THEN  RepeatFor  3  ((FunExt  THENA  Auto)))

---

Home Index