---

Step * 2 of Lemma comma-cat_wf

.....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'))} 
BY
{ (DProds
   THEN All Reduce
   THEN (DSetVars THEN DProds THEN Reduce 0)
   THEN (MemTypeCD THEN Reduce 0)
   THEN Auto
   THEN RW CatNormC 0
   THEN Auto
   THEN All Reduce
   THEN RWO "-4 -1" 0
   THEN Auto) }

---

Latex:

---

Latex:
.....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)  \mtimes{}  b:cat-ob(B)  \mtimes{}  (cat-arrow(C)  (S  a)  (T  b))@i
7.  v  :  a:cat-ob(A)  \mtimes{}  b:cat-ob(B)  \mtimes{}  (cat-arrow(C)  (S  a)  (T  b))@i
8.  w  :  a:cat-ob(A)  \mtimes{}  b:cat-ob(B)  \mtimes{}  (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'  \mtimes{}  (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')\}  @i
10.  gp  :  let  a,b,f  =  v  in 
let  a',b',f'  =  w  in 
\{gh:cat-arrow(A)  a  a'  \mtimes{}  (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')\}  @i
\mvdash{}  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'>  \mmember{}  let  a,b,f  =  u  in 
    let  a',b',f'  =  w  in 
    \{gh:cat-arrow(A)  a  a'  \mtimes{}  (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')\} 


By

---

Latex:
(DProds
  THEN  All  Reduce
  THEN  (DSetVars  THEN  DProds  THEN  Reduce  0)
  THEN  (MemTypeCD  THEN  Reduce  0)
  THEN  Auto
  THEN  RW  CatNormC  0
  THEN  Auto
  THEN  All  Reduce
  THEN  RWO  "-4  -1"  0
  THEN  Auto)

---

Home Index