---

Step * 1 1 of Lemma cat-final-isomorphic


1. C : SmallCategory
2. fnl1 : cat-ob(C)
3. fnl2 : cat-ob(C)
4. Final(fnl1)
5. Final(fnl2)
6. ∀[f,g:cat-arrow(C) fnl1 fnl2].  (f = g ∈ (cat-arrow(C) fnl1 fnl2))
7. f : cat-arrow(C) fnl1 fnl2
8. ∀[f,g:cat-arrow(C) fnl2 fnl1].  (f = g ∈ (cat-arrow(C) fnl2 fnl1))
9. g : cat-arrow(C) fnl2 fnl1
⊢ (cat-comp(C) fnl1 fnl2 fnl1 f g) = (cat-id(C) fnl1) ∈ (cat-arrow(C) fnl1 fnl1)
BY
{ (D 5 With ⌜fnl1⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  fnl1  :  cat-ob(C)
3.  fnl2  :  cat-ob(C)
4.  Final(fnl1)
5.  Final(fnl2)
6.  \mforall{}[f,g:cat-arrow(C)  fnl1  fnl2].    (f  =  g)
7.  f  :  cat-arrow(C)  fnl1  fnl2
8.  \mforall{}[f,g:cat-arrow(C)  fnl2  fnl1].    (f  =  g)
9.  g  :  cat-arrow(C)  fnl2  fnl1
\mvdash{}  (cat-comp(C)  fnl1  fnl2  fnl1  f  g)  =  (cat-id(C)  fnl1)


By

---

Latex:
(D  5  With  \mkleeneopen{}fnl1\mkleeneclose{}    THEN  Auto)

---

Home Index