Step
*
1
of Lemma
monad-extend-comp
1. C : SmallCategory
2. T : Functor(C;C)
3. M2 : A:cat-ob(C) ⟶ (cat-arrow(C) A (T A))
4. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
((cat-comp(C) A (T A) (T B) (M2 A) (T A B g)) = (cat-comp(C) A B (T B) g (M2 B)) ∈ (cat-arrow(C) A (T B)))
5. M3 : A:cat-ob(C) ⟶ (cat-arrow(C) (T (T A)) (T A))
6. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
((cat-comp(C) (T (T A)) (T A) (T B) (M3 A) (T A B g))
= (cat-comp(C) (T (T A)) (T (T B)) (T B) (T (T A) (T B) (T A B g)) (M3 B))
∈ (cat-arrow(C) (T (T A)) (T B)))
7. ∀X:cat-ob(C)
((cat-comp(C) (T X) (T (T X)) (T X) (M2 (T X)) (M3 X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X)))
8. ∀X:cat-ob(C)
((cat-comp(C) (T X) (T (T X)) (T X) (T X (T X) (M2 X)) (M3 X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X)))
9. ∀X:cat-ob(C)
((cat-comp(C) (T (T (T X))) (T (T X)) (T X) (M3 (T X)) (M3 X))
= (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (T X) (M3 X)) (M3 X))
∈ (cat-arrow(C) (T (T (T X))) (T X)))
10. x : cat-ob(C)
11. y : cat-ob(C)
12. z : cat-ob(C)
13. g : cat-arrow(C) x (T y)
14. h : cat-arrow(C) y (T z)
⊢ (cat-comp(C) (T x) (T (T z)) (T z)
(T x (T z) (cat-comp(C) x (T y) (T z) g (cat-comp(C) (T y) (T (T z)) (T z) (T y (T z) h) (M3 z))))
(M3 z))
= (cat-comp(C) (T x) (T y) (T z) (cat-comp(C) (T x) (T (T y)) (T y) (T x (T y) g) (M3 y))
(cat-comp(C) (T y) (T (T z)) (T z) (T y (T z) h) (M3 z)))
∈ (cat-arrow(C) (T x) (T z))
BY
{ ((RW CatNormC 0 THENA Auto) THEN All (Folds ``cat_comp functor_arrow``)) }
1
1. C : SmallCategory
2. T : Functor(C;C)
3. M2 : A:cat-ob(C) ⟶ (cat-arrow(C) A (T A))
4. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B. (T(g) o M2 A = M2 B o g ∈ (cat-arrow(C) A (T B)))
5. M3 : A:cat-ob(C) ⟶ (cat-arrow(C) (T (T A)) (T A))
6. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B. (T(g) o M3 A = M3 B o T(T(g)) ∈ (cat-arrow(C) (T (T A)) (T B)))
7. ∀X:cat-ob(C). (M3 X o M2 (T X) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X)))
8. ∀X:cat-ob(C). (M3 X o T(M2 X) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X)))
9. ∀X:cat-ob(C). (M3 X o M3 (T X) = M3 X o T(M3 X) ∈ (cat-arrow(C) (T (T (T X))) (T X)))
10. x : cat-ob(C)
11. y : cat-ob(C)
12. z : cat-ob(C)
13. g : cat-arrow(C) x (T y)
14. h : cat-arrow(C) y (T z)
⊢ M3 z o T(M3 z) o T(T(h)) o T(g) = M3 z o T(h) o M3 y o T(g) ∈ (cat-arrow(C) (T x) (T z))
Latex:
Latex:
1. C : SmallCategory
2. T : Functor(C;C)
3. M2 : A:cat-ob(C) {}\mrightarrow{} (cat-arrow(C) A (T A))
4. \mforall{}A,B:cat-ob(C). \mforall{}g:cat-arrow(C) A B.
((cat-comp(C) A (T A) (T B) (M2 A) (T A B g)) = (cat-comp(C) A B (T B) g (M2 B)))
5. M3 : A:cat-ob(C) {}\mrightarrow{} (cat-arrow(C) (T (T A)) (T A))
6. \mforall{}A,B:cat-ob(C). \mforall{}g:cat-arrow(C) A B.
((cat-comp(C) (T (T A)) (T A) (T B) (M3 A) (T A B g))
= (cat-comp(C) (T (T A)) (T (T B)) (T B) (T (T A) (T B) (T A B g)) (M3 B)))
7. \mforall{}X:cat-ob(C). ((cat-comp(C) (T X) (T (T X)) (T X) (M2 (T X)) (M3 X)) = (cat-id(C) (T X)))
8. \mforall{}X:cat-ob(C). ((cat-comp(C) (T X) (T (T X)) (T X) (T X (T X) (M2 X)) (M3 X)) = (cat-id(C) (T X)))
9. \mforall{}X:cat-ob(C)
((cat-comp(C) (T (T (T X))) (T (T X)) (T X) (M3 (T X)) (M3 X))
= (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (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 (T y)
14. h : cat-arrow(C) y (T z)
\mvdash{} (cat-comp(C) (T x) (T (T z)) (T z)
(T x (T z)
(cat-comp(C) x (T y) (T z) g (cat-comp(C) (T y) (T (T z)) (T z) (T y (T z) h) (M3 z))))
(M3 z))
= (cat-comp(C) (T x) (T y) (T z) (cat-comp(C) (T x) (T (T y)) (T y) (T x (T y) g) (M3 y))
(cat-comp(C) (T y) (T (T z)) (T z) (T y (T z) h) (M3 z)))
By
Latex:
((RW CatNormC 0 THENA Auto) THEN All (Folds ``cat\_comp functor\_arrow``))
Home
Index