---

Step * 1 of Lemma comma-cat_wf

.....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'))} 
BY
{ ((DProds THEN Reduce 0) THEN (MemTypeCD THEN Reduce 0) THEN Auto THEN RW CatNormC 0 THEN Auto) }

---

Latex:

---

Latex:
.....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)  \mtimes{}  b:cat-ob(B)  \mtimes{}  (cat-arrow(C)  (S  a)  (T  b))@i
\mvdash{}  let  a,b,f  =  x  in 
    <cat-id(A)  a,  cat-id(B)  b>  \mmember{}  let  a,b,f  =  x  in 
    let  a',b',f'  =  x  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  Reduce  0)  THEN  (MemTypeCD  THEN  Reduce  0)  THEN  Auto  THEN  RW  CatNormC  0  THEN  Auto)

---

Home Index