Proof of Nuprl Lemma : comma-cat

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)
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. a2 : cat-ob(A)
13. b2 : cat-ob(B)
14. z2 : cat-arrow(C) (ob(S) a2) (ob(T) b2)
15. a3 : cat-ob(A)
16. b3 : cat-ob(B)
17. w2 : cat-arrow(C) (ob(S) a3) (ob(T) b3)
18. f1 : cat-arrow(A) a a1
19. f2 : cat-arrow(B) b b1
20. (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))
21. g1 : cat-arrow(A) a1 a2
22. g2 : cat-arrow(B) b1 b2
23. (cat-comp(C) (ob(S) a1) (ob(T) b1) (ob(T) b2) y2 (arrow(T) b1 b2 (snd(<g1, g2>))))
= (cat-comp(C) (ob(S) a1) (ob(S) a2) (ob(T) b2) (arrow(S) a1 a2 (fst(<g1, g2>))) z2)
∈ (cat-arrow(C) (ob(S) a1) (ob(T) b2))
24. h1 : cat-arrow(A) a2 a3
25. h2 : cat-arrow(B) b2 b3
26. (cat-comp(C) (ob(S) a2) (ob(T) b2) (ob(T) b3) z2 (arrow(T) b2 b3 (snd(<h1, h2>))))
= (cat-comp(C) (ob(S) a2) (ob(S) a3) (ob(T) b3) (arrow(S) a2 a3 (fst(<h1, h2>))) w2)
∈ (cat-arrow(C) (ob(S) a2) (ob(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) (ob(S) a) (ob(T) b) (ob(T) b3) x2 (arrow(T) b b3 (snd(gh))))
   = (cat-comp(C) (ob(S) a) (ob(S) a3) (ob(T) b3) (arrow(S) a a3 (fst(gh))) w2)
   ∈ (cat-arrow(C) (ob(S) a) (ob(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) 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. a2 : cat-ob(A) 13. b2 : cat-ob(B) 14. z2 : cat-arrow(C) (ob(S) a2) (ob(T) b2) 15. a3 : cat-ob(A) 16. b3 : cat-ob(B) 17. w2 : cat-arrow(C) (ob(S) a3) (ob(T) b3) 18. f1 : cat-arrow(A) a a1 19. f2 : cat-arrow(B) b b1 20. (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) 21. g1 : cat-arrow(A) a1 a2 22. g2 : cat-arrow(B) b1 b2 23. (cat-comp(C) (ob(S) a1) (ob(T) b1) (ob(T) b2) y2 (arrow(T) b1 b2 (snd(<g1, g2>)))) = (cat-comp(C) (ob(S) a1) (ob(S) a2) (ob(T) b2) (arrow(S) a1 a2 (fst(<g1, g2>))) z2) 24. h1 : cat-arrow(A) a2 a3 25. h2 : cat-arrow(B) b2 b3 26. (cat-comp(C) (ob(S) a2) (ob(T) b2) (ob(T) b3) z2 (arrow(T) b2 b3 (snd(<h1, h2>)))) = (cat-comp(C) (ob(S) a2) (ob(S) a3) (ob(T) b3) (arrow(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