---

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)
7. b : cat-ob(B)
8. x2 : cat-arrow(C) (ob(S) a) (ob(T) b)
9. a1 : cat-ob(A)
10. b1 : cat-ob(B)
11. y2 : cat-arrow(C) (ob(S) a1) (ob(T) b1)
12. f1 : cat-arrow(A) a a1
13. f2 : cat-arrow(B) b b1
14. [%1] : (cat-comp(C) (ob(S) a) (ob(T) b) (ob(T) b1) x2 (arrow(T) b b1 (snd(<f1, f2>))))
= (cat-comp(C) (ob(S) a) (ob(S) a1) (ob(T) b1) (arrow(S) a a1 (fst(<f1, f2>))) y2)
∈ (cat-arrow(C) (ob(S) a) (ob(T) b1))
⊢ (<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) (ob(S) a) (ob(T) b) (ob(T) b1) x2 (arrow(T) b b1 (snd(gh))))
   = (cat-comp(C) (ob(S) a) (ob(S) a1) (ob(T) b1) (arrow(S) a a1 (fst(gh))) y2)
   ∈ (cat-arrow(C) (ob(S) a) (ob(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) (ob(S) a) (ob(T) b) (ob(T) b1) x2 (arrow(T) b b1 (snd(gh))))
     = (cat-comp(C) (ob(S) a) (ob(S) a1) (ob(T) b1) (arrow(S) a a1 (fst(gh))) y2)
     ∈ (cat-arrow(C) (ob(S) a) (ob(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)
7.  b  :  cat-ob(B)
8.  x2  :  cat-arrow(C)  (ob(S)  a)  (ob(T)  b)
9.  a1  :  cat-ob(A)
10.  b1  :  cat-ob(B)
11.  y2  :  cat-arrow(C)  (ob(S)  a1)  (ob(T)  b1)
12.  f1  :  cat-arrow(A)  a  a1
13.  f2  :  cat-arrow(B)  b  b1
14.  [\%1]  :  (cat-comp(C)  (ob(S)  a)  (ob(T)  b)  (ob(T)  b1)  x2  (arrow(T)  b  b1  (snd(<f1,  f2>))))
=  (cat-comp(C)  (ob(S)  a)  (ob(S)  a1)  (ob(T)  b1)  (arrow(S)  a  a1  (fst(<f1,  f2>)))  y2)
\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