---

Step * 1 2 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. (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)
BY
{ ((RWO "cat-comp-assoc" 0 THENA Auto)
   THEN (RW (AddrC [2;2] (RevLemmaC `cat-comp-assoc`)) 0 THENA Auto)
   THEN RWO  "-5" 0
   THEN Auto) }

---

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.  (cat-comp(C)  a  b  a  f  h)  =  (cat-id(C)  a)
9.  (cat-comp(C)  b  a  b  h  f)  =  (cat-id(C)  b)
10.  j  :  cat-arrow(C)  c  b
11.  (cat-comp(C)  b  c  b  g  j)  =  (cat-id(C)  b)
12.  (cat-comp(C)  c  b  c  j  g)  =  (cat-id(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)
\mvdash{}  (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)


By

---

Latex:
((RWO  "cat-comp-assoc"  0  THENA  Auto)
  THEN  (RW  (AddrC  [2;2]  (RevLemmaC  `cat-comp-assoc`))  0  THENA  Auto)
  THEN  RWO    "-5"  0
  THEN  Auto)

---

Home Index