---

Step * 1 of Lemma cat-comp-isomorphism


1. C : SmallCategory
2. a : cat-ob(C)
3. b : cat-ob(C)
4. c : cat-ob(C)
5. f : cat-arrow(C) a b
6. g : cat-arrow(C) b c
7. h : cat-arrow(C) b a
8. fh=1
9. hf=1
10. j : cat-arrow(C) c b
11. gj=1
12. jg=1
⊢ cat-isomorphism(C;a;c;cat-comp(C) a b c f g)
BY
{ ((D 0 With ⌜cat-comp(C) c b a j h⌝  THEN Auto) THEN All (Unfold `cat-inverse`)) }

1
1. C : SmallCategory
2. a : cat-ob(C)
3. b : cat-ob(C)
4. c : cat-ob(C)
5. f : cat-arrow(C) a b
6. g : cat-arrow(C) b c
7. h : cat-arrow(C) b a
8. (cat-comp(C) a b a f h) = (cat-id(C) a) ∈ (cat-arrow(C) a a)
9. (cat-comp(C) b a b h f) = (cat-id(C) b) ∈ (cat-arrow(C) b b)
10. j : cat-arrow(C) c b
11. (cat-comp(C) b c b g j) = (cat-id(C) b) ∈ (cat-arrow(C) b b)
12. (cat-comp(C) c b c j g) = (cat-id(C) c) ∈ (cat-arrow(C) c c)
⊢ (cat-comp(C) a c a (cat-comp(C) a b c f g) (cat-comp(C) c b a j h)) = (cat-id(C) a) ∈ (cat-arrow(C) a a)

2
1. C : SmallCategory
2. a : cat-ob(C)
3. b : cat-ob(C)
4. c : cat-ob(C)
5. f : cat-arrow(C) a b
6. g : cat-arrow(C) b c
7. h : cat-arrow(C) b a
8. (cat-comp(C) a b a f h) = (cat-id(C) a) ∈ (cat-arrow(C) a a)
9. (cat-comp(C) b a b h f) = (cat-id(C) b) ∈ (cat-arrow(C) b b)
10. j : cat-arrow(C) c b
11. (cat-comp(C) b c b g j) = (cat-id(C) b) ∈ (cat-arrow(C) b b)
12. (cat-comp(C) c b c j g) = (cat-id(C) c) ∈ (cat-arrow(C) c c)
13. (cat-comp(C) a c a (cat-comp(C) a b c f g) (cat-comp(C) c b a j h)) = (cat-id(C) a) ∈ (cat-arrow(C) a a)
⊢ (cat-comp(C) c a c (cat-comp(C) c b a j h) (cat-comp(C) a b c f g)) = (cat-id(C) c) ∈ (cat-arrow(C) c c)

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  a  :  cat-ob(C)
3.  b  :  cat-ob(C)
4.  c  :  cat-ob(C)
5.  f  :  cat-arrow(C)  a  b
6.  g  :  cat-arrow(C)  b  c
7.  h  :  cat-arrow(C)  b  a
8.  fh=1
9.  hf=1
10.  j  :  cat-arrow(C)  c  b
11.  gj=1
12.  jg=1
\mvdash{}  cat-isomorphism(C;a;c;cat-comp(C)  a  b  c  f  g)


By

---

Latex:
((D  0  With  \mkleeneopen{}cat-comp(C)  c  b  a  j  h\mkleeneclose{}    THEN  Auto)  THEN  All  (Unfold  `cat-inverse`))

---

Home Index