---

Step * of Lemma cat-initial-isomorphic

∀[C:SmallCategory]. ∀i1,i2:cat-ob(C).  (Initial(i1) ⇒ Initial(i2) ⇒ cat-isomorphic(C;i1;i2))
BY
{ (Auto
   THEN DupHyp (-2)
   THEN (D -1 With ⌜i2⌝  THENA Auto)
   THEN D -1
   THEN RenameVar `f' (-1)
   THEN D 0 With ⌜f⌝ 
   THEN Auto) }

1
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
⊢ cat-isomorphism(C;i1;i2;f)

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}i1,i2:cat-ob(C).    (Initial(i1)  {}\mRightarrow{}  Initial(i2)  {}\mRightarrow{}  cat-isomorphic(C;i1;i2))


By

---

Latex:
(Auto
  THEN  DupHyp  (-2)
  THEN  (D  -1  With  \mkleeneopen{}i2\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `f'  (-1)
  THEN  D  0  With  \mkleeneopen{}f\mkleeneclose{} 
  THEN  Auto)

---

Home Index