---

Step * 1 1 of Lemma cat-comp-isomorphism


1. C : SmallCategory@i'
2. a : cat-ob(C)@i
3. b : cat-ob(C)@i
4. c : cat-ob(C)@i
5. f : cat-arrow(C) a b@i
6. g : cat-arrow(C) b c@i
7. h : cat-arrow(C) b a@i
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@i
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)
BY
{ ((RWO "cat-comp-assoc<" 0 THENA Auto)
   THEN (RW (AddrC [2;1;2] (LemmaC `cat-comp-assoc`)) 0 THENA Auto)
   THEN RWO  "-2" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory@i'
2.  a  :  cat-ob(C)@i
3.  b  :  cat-ob(C)@i
4.  c  :  cat-ob(C)@i
5.  f  :  cat-arrow(C)  a  b@i
6.  g  :  cat-arrow(C)  b  c@i
7.  h  :  cat-arrow(C)  b  a@i
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@i
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)
\mvdash{}  (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)


By

---

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

---

Home Index