Step
*
1
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
⊢ cat-isomorphism(C;i1;i2;f)
BY
{ (DupHyp (-3)
THEN (D -1 With ⌜i1⌝ THENA Auto)
THEN D -1
THEN RenameVar `g' (-1)
THEN D 0 With ⌜g⌝
THEN Auto
THEN UnfoldTopAb 0) }
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
8. ∀[f,g:cat-arrow(C) i2 i1]. (f = g ∈ (cat-arrow(C) i2 i1))
9. g : cat-arrow(C) i2 i1
⊢ (cat-comp(C) i1 i2 i1 f g) = (cat-id(C) i1) ∈ (cat-arrow(C) i1 i1)
2
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)
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
\mvdash{} cat-isomorphism(C;i1;i2;f)
By
Latex:
(DupHyp (-3)
THEN (D -1 With \mkleeneopen{}i1\mkleeneclose{} THENA Auto)
THEN D -1
THEN RenameVar `g' (-1)
THEN D 0 With \mkleeneopen{}g\mkleeneclose{}
THEN Auto
THEN UnfoldTopAb 0)
Home
Index