Proof of Nuprl Lemma : comma-cat

Step * of Lemma comma-cat_wf

∀[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) (ob(S) a) (ob(T) b))
⊢ 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) (ob(S) a) (ob(T) b) (ob(T) b') f (arrow(T) b b' (snd(gh))))
   = (cat-comp(C) (ob(S) a) (ob(S) a') (ob(T) b') (arrow(S) a a' (fst(gh))) f')
   ∈ (cat-arrow(C) (ob(S) a) (ob(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) (ob(S) a) (ob(T) b))
7. v : a:cat-ob(A) × b:cat-ob(B) × (cat-arrow(C) (ob(S) a) (ob(T) b))
8. w : a:cat-ob(A) × b:cat-ob(B) × (cat-arrow(C) (ob(S) a) (ob(T) b))
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) (ob(S) a) (ob(T) b) (ob(T) b') f (arrow(T) b b' (snd(gh))))
= (cat-comp(C) (ob(S) a) (ob(S) a') (ob(T) b') (arrow(S) a a' (fst(gh))) f')
∈ (cat-arrow(C) (ob(S) a) (ob(T) b'))}
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) (ob(S) a) (ob(T) b) (ob(T) b') f (arrow(T) b b' (snd(gh))))
= (cat-comp(C) (ob(S) a) (ob(S) a') (ob(T) b') (arrow(S) a a' (fst(gh))) f')
∈ (cat-arrow(C) (ob(S) a) (ob(T) b'))}
⊢ 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) (ob(S) a) (ob(T) b) (ob(T) b') f (arrow(T) b b' (snd(gh))))
   = (cat-comp(C) (ob(S) a) (ob(S) a') (ob(T) b') (arrow(S) a a' (fst(gh))) f')
   ∈ (cat-arrow(C) (ob(S) a) (ob(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)
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))} )

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

Latex:

Latex:
\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