---

Step * 1 2 of Lemma cat-initial-isomorphic


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index