---

Step * 4 of Lemma comma-cat_wf


1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. S : Functor(A;C)
5. T : Functor(B;C)
6. a : cat-ob(A)@i
7. b : cat-ob(B)@i
8. x2 : cat-arrow(C) (S a) (T b)@i
9. a1 : cat-ob(A)@i
10. b1 : cat-ob(B)@i
11. y2 : cat-arrow(C) (S a1) (T b1)@i
12. a2 : cat-ob(A)@i
13. b2 : cat-ob(B)@i
14. z2 : cat-arrow(C) (S a2) (T b2)@i
15. a3 : cat-ob(A)@i
16. b3 : cat-ob(B)@i
17. w2 : cat-arrow(C) (S a3) (T b3)@i
18. f1 : cat-arrow(A) a a1@i
19. f2 : cat-arrow(B) b b1@i
20. (cat-comp(C) (S a) (T b) (T b1) x2 (T b b1 (snd(<f1, f2>))))
= (cat-comp(C) (S a) (S a1) (T b1) (S a a1 (fst(<f1, f2>))) y2)
∈ (cat-arrow(C) (S a) (T b1))
21. g1 : cat-arrow(A) a1 a2@i
22. g2 : cat-arrow(B) b1 b2@i
23. (cat-comp(C) (S a1) (T b1) (T b2) y2 (T b1 b2 (snd(<g1, g2>))))
= (cat-comp(C) (S a1) (S a2) (T b2) (S a1 a2 (fst(<g1, g2>))) z2)
∈ (cat-arrow(C) (S a1) (T b2))
24. h1 : cat-arrow(A) a2 a3@i
25. h2 : cat-arrow(B) b2 b3@i
26. (cat-comp(C) (S a2) (T b2) (T b3) z2 (T b2 b3 (snd(<h1, h2>))))
= (cat-comp(C) (S a2) (S a3) (T b3) (S a2 a3 (fst(<h1, h2>))) w2)
∈ (cat-arrow(C) (S a2) (T b3))
⊢ <cat-comp(A) a a2 a3 (cat-comp(A) a a1 a2 f1 g1) h1, cat-comp(B) b b2 b3 (cat-comp(B) b b1 b2 f2 g2) h2>
= <cat-comp(A) a a1 a3 f1 (cat-comp(A) a1 a2 a3 g1 h1), cat-comp(B) b b1 b3 f2 (cat-comp(B) b1 b2 b3 g2 h2)>
∈ {gh:cat-arrow(A) a a3 × (cat-arrow(B) b b3)| 
   (cat-comp(C) (S a) (T b) (T b3) x2 (T b b3 (snd(gh))))
   = (cat-comp(C) (S a) (S a3) (T b3) (S a a3 (fst(gh))) w2)
   ∈ (cat-arrow(C) (S a) (T b3))} 
BY
{ ((EqTypeCD THEN All Reduce THEN Auto)
   THEN All (Fold  `cat-square-commutes`)
   THEN (FLemma `cat-square-commutes-comp` [-7;-4] THENA Auto)
   THEN (FLemma `cat-square-commutes-comp` [-1;-2] THENA Auto)
   THEN NthHypEq (-1)
   THEN EqCDA
   THEN RW CatNormC 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  SmallCategory
2.  B  :  SmallCategory
3.  C  :  SmallCategory
4.  S  :  Functor(A;C)
5.  T  :  Functor(B;C)
6.  a  :  cat-ob(A)@i
7.  b  :  cat-ob(B)@i
8.  x2  :  cat-arrow(C)  (S  a)  (T  b)@i
9.  a1  :  cat-ob(A)@i
10.  b1  :  cat-ob(B)@i
11.  y2  :  cat-arrow(C)  (S  a1)  (T  b1)@i
12.  a2  :  cat-ob(A)@i
13.  b2  :  cat-ob(B)@i
14.  z2  :  cat-arrow(C)  (S  a2)  (T  b2)@i
15.  a3  :  cat-ob(A)@i
16.  b3  :  cat-ob(B)@i
17.  w2  :  cat-arrow(C)  (S  a3)  (T  b3)@i
18.  f1  :  cat-arrow(A)  a  a1@i
19.  f2  :  cat-arrow(B)  b  b1@i
20.  (cat-comp(C)  (S  a)  (T  b)  (T  b1)  x2  (T  b  b1  (snd(<f1,  f2>))))
=  (cat-comp(C)  (S  a)  (S  a1)  (T  b1)  (S  a  a1  (fst(<f1,  f2>)))  y2)
21.  g1  :  cat-arrow(A)  a1  a2@i
22.  g2  :  cat-arrow(B)  b1  b2@i
23.  (cat-comp(C)  (S  a1)  (T  b1)  (T  b2)  y2  (T  b1  b2  (snd(<g1,  g2>))))
=  (cat-comp(C)  (S  a1)  (S  a2)  (T  b2)  (S  a1  a2  (fst(<g1,  g2>)))  z2)
24.  h1  :  cat-arrow(A)  a2  a3@i
25.  h2  :  cat-arrow(B)  b2  b3@i
26.  (cat-comp(C)  (S  a2)  (T  b2)  (T  b3)  z2  (T  b2  b3  (snd(<h1,  h2>))))
=  (cat-comp(C)  (S  a2)  (S  a3)  (T  b3)  (S  a2  a3  (fst(<h1,  h2>)))  w2)
\mvdash{}  <cat-comp(A)  a  a2  a3  (cat-comp(A)  a  a1  a2  f1  g1)  h1
    ,  cat-comp(B)  b  b2  b3  (cat-comp(B)  b  b1  b2  f2  g2)  h2
    >
=  <cat-comp(A)  a  a1  a3  f1  (cat-comp(A)  a1  a2  a3  g1  h1)
    ,  cat-comp(B)  b  b1  b3  f2  (cat-comp(B)  b1  b2  b3  g2  h2)
    >


By

---

Latex:
((EqTypeCD  THEN  All  Reduce  THEN  Auto)
  THEN  All  (Fold    `cat-square-commutes`)
  THEN  (FLemma  `cat-square-commutes-comp`  [-7;-4]  THENA  Auto)
  THEN  (FLemma  `cat-square-commutes-comp`  [-1;-2]  THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  EqCDA
  THEN  RW  CatNormC  0
  THEN  Auto)

---

Home Index