---

Step * 1 of Lemma nat-trans-assoc-equation

.....subterm..... T:t
2:n
1. C : SmallCategory
2. D : SmallCategory
3. F : Functor(C;D)
4. G : Functor(C;D)
5. T : nat-trans(C;D;F;G)
6. A : cat-ob(C)
7. B : cat-ob(C)
8. B' : cat-ob(C)
9. g : cat-arrow(C) A B
10. h : cat-arrow(C) B B'
11. (cat-comp(D) (F A) (F B') (G B') (cat-comp(D) (F A) (F B) (F B') (F A B g) (F B B' h)) (T B'))
= (cat-comp(D) (F A) (F B') (G B') (cat-comp(D) (F A) (F B) (F B') (F A B g) (F B B' h)) (T B'))
∈ (cat-arrow(D) (F A) (G B'))
⊢ (cat-comp(D) (F A) (G B) (G B') (cat-comp(D) (F A) (F B) (G B) (F A B g) (T B)) (G B B' h))
= (cat-comp(D) (F A) (F B') (G B') (cat-comp(D) (F A) (F B) (F B') (F A B g) (F B B' h)) (T B'))
∈ (cat-arrow(D) (F A) (G B'))
BY
{ (DVar `T'
   THEN (RWO "6<" 0 THENA Auto)
   THEN (RWO "cat-comp-assoc" 0 THENA Auto)
   THEN (RWO "6<" 0 THENA Auto)
   THEN (RWO "cat-comp-assoc<" 0 THENA Auto)
   THEN RepeatFor 2 (EqCDA)
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  C  :  SmallCategory
2.  D  :  SmallCategory
3.  F  :  Functor(C;D)
4.  G  :  Functor(C;D)
5.  T  :  nat-trans(C;D;F;G)
6.  A  :  cat-ob(C)
7.  B  :  cat-ob(C)
8.  B'  :  cat-ob(C)
9.  g  :  cat-arrow(C)  A  B
10.  h  :  cat-arrow(C)  B  B'
11.  (cat-comp(D)  (F  A)  (F  B')  (G  B')  (cat-comp(D)  (F  A)  (F  B)  (F  B')  (F  A  B  g)  (F  B  B'  h))  (T  B'))
=  (cat-comp(D)  (F  A)  (F  B')  (G  B')  (cat-comp(D)  (F  A)  (F  B)  (F  B')  (F  A  B  g)  (F  B  B'  h))  (T  B'))
\mvdash{}  (cat-comp(D)  (F  A)  (G  B)  (G  B')  (cat-comp(D)  (F  A)  (F  B)  (G  B)  (F  A  B  g)  (T  B))  (G  B  B'  h))
=  (cat-comp(D)  (F  A)  (F  B')  (G  B')  (cat-comp(D)  (F  A)  (F  B)  (F  B')  (F  A  B  g)  (F  B  B'  h))  (T  B'))


By

---

Latex:
(DVar  `T'
  THEN  (RWO  "6<"  0  THENA  Auto)
  THEN  (RWO  "cat-comp-assoc"  0  THENA  Auto)
  THEN  (RWO  "6<"  0  THENA  Auto)
  THEN  (RWO  "cat-comp-assoc<"  0  THENA  Auto)
  THEN  RepeatFor  2  (EqCDA)
  THEN  Auto)

---

Home Index