Step * 1 of Lemma monad-extend-comp


1. SmallCategory
2. Functor(C;C)
3. M2 A:cat-ob(C) ⟶ (cat-arrow(C) (ob(T) A))
4. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) B.
     ((cat-comp(C) (ob(T) A) (ob(T) B) (M2 A) (arrow(T) g))
     (cat-comp(C) (ob(T) B) (M2 B))
     ∈ (cat-arrow(C) (ob(T) B)))
5. M3 A:cat-ob(C) ⟶ (cat-arrow(C) (ob(T) (ob(T) A)) (ob(T) A))
6. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) B.
     ((cat-comp(C) (ob(T) (ob(T) A)) (ob(T) A) (ob(T) B) (M3 A) (arrow(T) g))
     (cat-comp(C) (ob(T) (ob(T) A)) (ob(T) (ob(T) B)) (ob(T) B) (arrow(T) (ob(T) A) (ob(T) B) (arrow(T) g)) 
        (M3 B))
     ∈ (cat-arrow(C) (ob(T) (ob(T) A)) (ob(T) B)))
7. ∀X:cat-ob(C)
     ((cat-comp(C) (ob(T) X) (ob(T) (ob(T) X)) (ob(T) X) (M2 (ob(T) X)) (M3 X))
     (cat-id(C) (ob(T) X))
     ∈ (cat-arrow(C) (ob(T) X) (ob(T) X)))
8. ∀X:cat-ob(C)
     ((cat-comp(C) (ob(T) X) (ob(T) (ob(T) X)) (ob(T) X) (arrow(T) (ob(T) X) (M2 X)) (M3 X))
     (cat-id(C) (ob(T) X))
     ∈ (cat-arrow(C) (ob(T) X) (ob(T) X)))
9. ∀X:cat-ob(C)
     ((cat-comp(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) (ob(T) X)) (ob(T) X) (M3 (ob(T) X)) (M3 X))
     (cat-comp(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) (ob(T) X)) (ob(T) X) (arrow(T) (ob(T) (ob(T) X)) (ob(T) X) (M3 X)) 
        (M3 X))
     ∈ (cat-arrow(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) X)))
10. cat-ob(C)
11. cat-ob(C)
12. cat-ob(C)
13. cat-arrow(C) (ob(T) y)
14. cat-arrow(C) (ob(T) z)
⊢ (cat-comp(C) (ob(T) x) (ob(T) (ob(T) z)) (ob(T) z) 
   (arrow(T) (ob(T) z) 
    (cat-comp(C) (ob(T) y) (ob(T) z) 
     (cat-comp(C) (ob(T) y) (ob(T) (ob(T) z)) (ob(T) z) (arrow(T) (ob(T) z) h) (M3 z)))) 
   (M3 z))
(cat-comp(C) (ob(T) x) (ob(T) y) (ob(T) z) 
   (cat-comp(C) (ob(T) x) (ob(T) (ob(T) y)) (ob(T) y) (arrow(T) (ob(T) y) g) (M3 y)) 
   (cat-comp(C) (ob(T) y) (ob(T) (ob(T) z)) (ob(T) z) (arrow(T) (ob(T) z) h) (M3 z)))
∈ (cat-arrow(C) (ob(T) x) (ob(T) z))
BY
((RW CatNormC THENA Auto) THEN All (Folds ``cat_comp functor_arrow``)) }

1
1. SmallCategory
2. Functor(C;C)
3. M2 A:cat-ob(C) ⟶ (cat-arrow(C) (ob(T) A))
4. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) B.  (T(g) M2 M2 g ∈ (cat-arrow(C) (ob(T) B)))
5. M3 A:cat-ob(C) ⟶ (cat-arrow(C) (ob(T) (ob(T) A)) (ob(T) A))
6. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) B.  (T(g) M3 M3 T(T(g)) ∈ (cat-arrow(C) (ob(T) (ob(T) A)) (ob(T) B)))
7. ∀X:cat-ob(C). (M3 M2 (ob(T) X) (cat-id(C) (ob(T) X)) ∈ (cat-arrow(C) (ob(T) X) (ob(T) X)))
8. ∀X:cat-ob(C). (M3 T(M2 X) (cat-id(C) (ob(T) X)) ∈ (cat-arrow(C) (ob(T) X) (ob(T) X)))
9. ∀X:cat-ob(C). (M3 M3 (ob(T) X) M3 T(M3 X) ∈ (cat-arrow(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) X)))
10. cat-ob(C)
11. cat-ob(C)
12. cat-ob(C)
13. cat-arrow(C) (ob(T) y)
14. cat-arrow(C) (ob(T) z)
⊢ M3 T(M3 z) T(T(h)) T(g) M3 T(h) M3 T(g) ∈ (cat-arrow(C) (ob(T) x) (ob(T) z))


Latex:


Latex:

1.  C  :  SmallCategory
2.  T  :  Functor(C;C)
3.  M2  :  A:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(C)  A  (ob(T)  A))
4.  \mforall{}A,B:cat-ob(C).  \mforall{}g:cat-arrow(C)  A  B.
          ((cat-comp(C)  A  (ob(T)  A)  (ob(T)  B)  (M2  A)  (arrow(T)  A  B  g))
          =  (cat-comp(C)  A  B  (ob(T)  B)  g  (M2  B)))
5.  M3  :  A:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(C)  (ob(T)  (ob(T)  A))  (ob(T)  A))
6.  \mforall{}A,B:cat-ob(C).  \mforall{}g:cat-arrow(C)  A  B.
          ((cat-comp(C)  (ob(T)  (ob(T)  A))  (ob(T)  A)  (ob(T)  B)  (M3  A)  (arrow(T)  A  B  g))
          =  (cat-comp(C)  (ob(T)  (ob(T)  A))  (ob(T)  (ob(T)  B))  (ob(T)  B) 
                (arrow(T)  (ob(T)  A)  (ob(T)  B)  (arrow(T)  A  B  g)) 
                (M3  B)))
7.  \mforall{}X:cat-ob(C)
          ((cat-comp(C)  (ob(T)  X)  (ob(T)  (ob(T)  X))  (ob(T)  X)  (M2  (ob(T)  X))  (M3  X))
          =  (cat-id(C)  (ob(T)  X)))
8.  \mforall{}X:cat-ob(C)
          ((cat-comp(C)  (ob(T)  X)  (ob(T)  (ob(T)  X))  (ob(T)  X)  (arrow(T)  X  (ob(T)  X)  (M2  X))  (M3  X))
          =  (cat-id(C)  (ob(T)  X)))
9.  \mforall{}X:cat-ob(C)
          ((cat-comp(C)  (ob(T)  (ob(T)  (ob(T)  X)))  (ob(T)  (ob(T)  X))  (ob(T)  X)  (M3  (ob(T)  X))  (M3  X))
          =  (cat-comp(C)  (ob(T)  (ob(T)  (ob(T)  X)))  (ob(T)  (ob(T)  X))  (ob(T)  X) 
                (arrow(T)  (ob(T)  (ob(T)  X))  (ob(T)  X)  (M3  X)) 
                (M3  X)))
10.  x  :  cat-ob(C)
11.  y  :  cat-ob(C)
12.  z  :  cat-ob(C)
13.  g  :  cat-arrow(C)  x  (ob(T)  y)
14.  h  :  cat-arrow(C)  y  (ob(T)  z)
\mvdash{}  (cat-comp(C)  (ob(T)  x)  (ob(T)  (ob(T)  z))  (ob(T)  z) 
      (arrow(T)  x  (ob(T)  z) 
        (cat-comp(C)  x  (ob(T)  y)  (ob(T)  z)  g 
          (cat-comp(C)  (ob(T)  y)  (ob(T)  (ob(T)  z))  (ob(T)  z)  (arrow(T)  y  (ob(T)  z)  h)  (M3  z)))) 
      (M3  z))
=  (cat-comp(C)  (ob(T)  x)  (ob(T)  y)  (ob(T)  z) 
      (cat-comp(C)  (ob(T)  x)  (ob(T)  (ob(T)  y))  (ob(T)  y)  (arrow(T)  x  (ob(T)  y)  g)  (M3  y)) 
      (cat-comp(C)  (ob(T)  y)  (ob(T)  (ob(T)  z))  (ob(T)  z)  (arrow(T)  y  (ob(T)  z)  h)  (M3  z)))


By


Latex:
((RW  CatNormC  0  THENA  Auto)  THEN  All  (Folds  ``cat\_comp  functor\_arrow``))




Home Index