---

Step * 1 1 1 of Lemma poset-extend-unique


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. ∀x:cat-ob(poset-cat(I)). ((F2 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F1 x)) ∈ (cat-arrow(C) (F1 x) (F1 x)))
8. ∀x,y,z:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) x y. ∀g:cat-arrow(poset-cat(I)) y z.
     ((F2 x z (cat-comp(poset-cat(I)) x y z f g))
     = (cat-comp(C) (F1 x) (F1 y) (F1 z) (F2 x y f) (F2 y z g))
     ∈ (cat-arrow(C) (F1 x) (F1 z)))
9. F : cat-ob(poset-cat(I)) ⟶ cat-ob(C)
10. 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))
11. ∀x:cat-ob(poset-cat(I)). ((G1 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F x)) ∈ (cat-arrow(C) (F x) (F x)))
12. ∀x,y,z:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) x y. ∀g:cat-arrow(poset-cat(I)) y z.
      ((G1 x z (cat-comp(poset-cat(I)) x y z f g))
      = (cat-comp(C) (F x) (F y) (F z) (G1 x y f) (G1 y z g))
      ∈ (cat-arrow(C) (F x) (F z)))
13. F1 = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
14. ∀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))))
15. F = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
16. ∀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))))
17. x : cat-ob(poset-cat(I))@i
18. y : cat-ob(poset-cat(I))@i
19. p : cat-arrow(poset-cat(I)) x y@i
20. x = y ∈ cat-ob(poset-cat(I))
21. ((F2 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F1 x)) ∈ (cat-arrow(C) (F1 x) (F1 x)))
∧ ((G1 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F x)) ∈ (cat-arrow(C) (F x) (F x)))
22. (F2 x x (cat-id(poset-cat(I)) x)) = (G1 x x (cat-id(poset-cat(I)) x)) ∈ (cat-arrow(C) (F1 x) (F1 x))
⊢ (F2 x y p) = (G1 x y p) ∈ (cat-arrow(C) (F1 x) (F1 y))
BY
{ TACTIC:TACTIC:((Assert p = (cat-id(poset-cat(I)) x) ∈ (cat-arrow(poset-cat(I)) x y) BY
                        (BLemma `poset-cat-arrow-unique` THEN Auto))
                 THEN NthHypEq (-2)
                 THEN RepeatFor 2 (EqCDA)
                 THEN Auto) }

---

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.  F1  :  cat-ob(poset-cat(I))  {}\mrightarrow{}  cat-ob(C)
6.  F2  :  x:cat-ob(poset-cat(I))
{}\mrightarrow{}  y:cat-ob(poset-cat(I))
{}\mrightarrow{}  (cat-arrow(poset-cat(I))  x  y)
{}\mrightarrow{}  (cat-arrow(C)  (F1  x)  (F1  y))
7.  \mforall{}x:cat-ob(poset-cat(I)).  ((F2  x  x  (cat-id(poset-cat(I))  x))  =  (cat-id(C)  (F1  x)))
8.  \mforall{}x,y,z:cat-ob(poset-cat(I)).  \mforall{}f:cat-arrow(poset-cat(I))  x  y.  \mforall{}g:cat-arrow(poset-cat(I))  y  z.
          ((F2  x  z  (cat-comp(poset-cat(I))  x  y  z  f  g))
          =  (cat-comp(C)  (F1  x)  (F1  y)  (F1  z)  (F2  x  y  f)  (F2  y  z  g)))
9.  F  :  cat-ob(poset-cat(I))  {}\mrightarrow{}  cat-ob(C)
10.  G1  :  x:cat-ob(poset-cat(I))
{}\mrightarrow{}  y:cat-ob(poset-cat(I))
{}\mrightarrow{}  (cat-arrow(poset-cat(I))  x  y)
{}\mrightarrow{}  (cat-arrow(C)  (F  x)  (F  y))
11.  \mforall{}x:cat-ob(poset-cat(I)).  ((G1  x  x  (cat-id(poset-cat(I))  x))  =  (cat-id(C)  (F  x)))
12.  \mforall{}x,y,z:cat-ob(poset-cat(I)).  \mforall{}f:cat-arrow(poset-cat(I))  x  y.  \mforall{}g:cat-arrow(poset-cat(I))  y  z.
            ((G1  x  z  (cat-comp(poset-cat(I))  x  y  z  f  g))
            =  (cat-comp(C)  (F  x)  (F  y)  (F  z)  (G1  x  y  f)  (G1  y  z  g)))
13.  F1  =  L
14.  \mforall{}i:nameset(I).  \mforall{}c:\{c:name-morph(I;[])|  (c  i)  =  0\}  .    ((F2  c  flip(c;i)  (\mlambda{}x.Ax))  =  (E  i  c))
15.  F  =  L
16.  \mforall{}i:nameset(I).  \mforall{}c:\{c:name-morph(I;[])|  (c  i)  =  0\}  .    ((G1  c  flip(c;i)  (\mlambda{}x.Ax))  =  (E  i  c))
17.  x  :  cat-ob(poset-cat(I))@i
18.  y  :  cat-ob(poset-cat(I))@i
19.  p  :  cat-arrow(poset-cat(I))  x  y@i
20.  x  =  y
21.  ((F2  x  x  (cat-id(poset-cat(I))  x))  =  (cat-id(C)  (F1  x)))
\mwedge{}  ((G1  x  x  (cat-id(poset-cat(I))  x))  =  (cat-id(C)  (F  x)))
22.  (F2  x  x  (cat-id(poset-cat(I))  x))  =  (G1  x  x  (cat-id(poset-cat(I))  x))
\mvdash{}  (F2  x  y  p)  =  (G1  x  y  p)


By

---

Latex:
TACTIC:TACTIC:((Assert  p  =  (cat-id(poset-cat(I))  x)  BY
                                            (BLemma  `poset-cat-arrow-unique`  THEN  Auto))
                              THEN  NthHypEq  (-2)
                              THEN  RepeatFor  2  (EqCDA)
                              THEN  Auto)

---

Home Index