Proof of Nuprl Lemma : comma-cat

Step * of Lemma comma-cat_wf

No Annotations
∀[A,B,C:SmallCategory]. ∀[S:Functor(A;C)]. ∀[T:Functor(B;C)].  ((S ↓ T) ∈ SmallCategory)
BY
{ (Auto
   THEN Unfold `comma-cat` 0
   THEN At ⌜Type⌝ MemCD⋅
   THEN Try (QuickAuto)
   THEN Try (RepeatFor 7 (((D 0 THENA Auto) THEN DSetVars THEN DProds THEN Reduce 0)))
   THEN Try (RepeatFor 3 (((D 0 THENA Auto) THEN DSetVars THEN DProds THEN Reduce 0)))) }

1
.....subterm..... T:t
3:n
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. S : Functor(A;C)
5. T : Functor(B;C)
6. x : a:cat-ob(A) × b:cat-ob(B) × (cat-arrow(C) (S a) (T b))@i
⊢ let a,b,f = x in
  <cat-id(A) a, cat-id(B) b> ∈ let a,b,f = x in
  let a',b',f' = x in
  {gh:cat-arrow(A) a a' × (cat-arrow(B) b b')|
   (cat-comp(C) (S a) (T b) (T b') f (T b b' (snd(gh))))
   = (cat-comp(C) (S a) (S a') (T b') (S a a' (fst(gh))) f')
   ∈ (cat-arrow(C) (S a) (T b'))}

2
.....subterm..... T:t
4:n
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. S : Functor(A;C)
5. T : Functor(B;C)
6. u : a:cat-ob(A) × b:cat-ob(B) × (cat-arrow(C) (S a) (T b))@i
7. v : a:cat-ob(A) × b:cat-ob(B) × (cat-arrow(C) (S a) (T b))@i
8. w : a:cat-ob(A) × b:cat-ob(B) × (cat-arrow(C) (S a) (T b))@i
9. fp : let a,b,f = u in
let a',b',f' = v in
{gh:cat-arrow(A) a a' × (cat-arrow(B) b b')|
(cat-comp(C) (S a) (T b) (T b') f (T b b' (snd(gh))))
= (cat-comp(C) (S a) (S a') (T b') (S a a' (fst(gh))) f')
∈ (cat-arrow(C) (S a) (T b'))} @i
10. gp : let a,b,f = v in
let a',b',f' = w in
{gh:cat-arrow(A) a a' × (cat-arrow(B) b b')|
(cat-comp(C) (S a) (T b) (T b') f (T b b' (snd(gh))))
= (cat-comp(C) (S a) (S a') (T b') (S a a' (fst(gh))) f')
∈ (cat-arrow(C) (S a) (T b'))} @i
⊢ let a,b,x = u in
  let a',b',x' = v in
  let a'',b'',x'' = w in
  let f,g = fp
  in let f',g' = gp
     in <cat-comp(A) a a' a'' f f', cat-comp(B) b b' b'' g g'> ∈ let a,b,f = u in
  let a',b',f' = w in
  {gh:cat-arrow(A) a a' × (cat-arrow(B) b b')|
   (cat-comp(C) (S a) (T b) (T b') f (T b b' (snd(gh))))
   = (cat-comp(C) (S a) (S a') (T b') (S a a' (fst(gh))) f')
   ∈ (cat-arrow(C) (S a) (T b'))}

3
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))} )

4
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))}

Latex:

Latex:
No Annotations \mforall{}[A,B,C:SmallCategory]. \mforall{}[S:Functor(A;C)]. \mforall{}[T:Functor(B;C)]. ((S \mdownarrow{} T) \mmember{} SmallCategory) By Latex: (Auto THEN Unfold `comma-cat` 0 THEN At \mkleeneopen{}Type\mkleeneclose{} MemCD\mcdot{} THEN Try (QuickAuto) THEN Try (RepeatFor 7 (((D 0 THENA Auto) THEN DSetVars THEN DProds THEN Reduce 0))) THEN Try (RepeatFor 3 (((D 0 THENA Auto) THEN DSetVars THEN DProds THEN Reduce 0)))) Home Index