---

Step * 3 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. f1 : cat-arrow(A) a a1@i
13. f2 : cat-arrow(B) b b1@i
14. [%1] : (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))@i
⊢ (<cat-comp(A) a a a1 (cat-id(A) a) f1, cat-comp(B) b b b1 (cat-id(B) b) f2>
= <f1, f2>
∈ {gh:cat-arrow(A) a a1 × (cat-arrow(B) b b1)| 
   (cat-comp(C) (S a) (T b) (T b1) x2 (T b b1 (snd(gh))))
   = (cat-comp(C) (S a) (S a1) (T b1) (S a a1 (fst(gh))) y2)
   ∈ (cat-arrow(C) (S a) (T b1))} )
∧ (<cat-comp(A) a a1 a1 f1 (cat-id(A) a1), cat-comp(B) b b1 b1 f2 (cat-id(B) b1)>
  = <f1, f2>
  ∈ {gh:cat-arrow(A) a a1 × (cat-arrow(B) b b1)| 
     (cat-comp(C) (S a) (T b) (T b1) x2 (T b b1 (snd(gh))))
     = (cat-comp(C) (S a) (S a1) (T b1) (S a a1 (fst(gh))) y2)
     ∈ (cat-arrow(C) (S a) (T b1))} )
BY
{ (DAnd 0⋅ THEN EqTypeCD THEN Reduce 0 THEN Auto 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.  f1  :  cat-arrow(A)  a  a1@i
13.  f2  :  cat-arrow(B)  b  b1@i
14.  [\%1]  :  (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)@i
\mvdash{}  (<cat-comp(A)  a  a  a1  (cat-id(A)  a)  f1,  cat-comp(B)  b  b  b1  (cat-id(B)  b)  f2>  =  <f1,  f2>)
\mwedge{}  (<cat-comp(A)  a  a1  a1  f1  (cat-id(A)  a1),  cat-comp(B)  b  b1  b1  f2  (cat-id(B)  b1)>  =  <f1,  f2>)


By

---

Latex:
(DAnd  0\mcdot{}  THEN  EqTypeCD  THEN  Reduce  0  THEN  Auto  THEN  RW  CatNormC  0  THEN  Auto)

---

Home Index