Step * 1 1 1 of Lemma equal-monads


1. SmallCategory
2. T1 Functor(C;C)
3. M7 A:cat-ob(C) ⟶ (cat-arrow(C) (1 A) (T1 A))
4. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) B.
     ((cat-comp(C) (1 A) (T1 A) (T1 B) (M7 A) (T1 g))
     (cat-comp(C) (1 A) (1 B) (T1 B) (1 g) (M7 B))
     ∈ (cat-arrow(C) (1 A) (T1 B)))
5. M8 nat-trans(C;C;functor-comp(T1;T1);T1)
6. (∀X:cat-ob(C)
      ((cat-comp(C) (T1 X) (T1 (T1 X)) (T1 X) (M7 (T1 X)) (M8 X)) (cat-id(C) (T1 X)) ∈ (cat-arrow(C) (T1 X) (T1 X))))
∧ (∀X:cat-ob(C)
     ((cat-comp(C) (T1 X) (T1 (T1 X)) (T1 X) (T1 (T1 X) (M7 X)) (M8 X))
     (cat-id(C) (T1 X))
     ∈ (cat-arrow(C) (T1 X) (T1 X))))
∧ (∀X:cat-ob(C)
     ((cat-comp(C) (T1 (T1 (T1 X))) (T1 (T1 X)) (T1 X) (M8 (T1 X)) (M8 X))
     (cat-comp(C) (T1 (T1 (T1 X))) (T1 (T1 X)) (T1 X) (T1 (T1 (T1 X)) (T1 X) (M8 X)) (M8 X))
     ∈ (cat-arrow(C) (T1 (T1 (T1 X))) (T1 X))))
7. Functor(C;C)
8. M5 nat-trans(C;C;1;T)
9. M6 nat-trans(C;C;functor-comp(T;T);T)
10. (∀X:cat-ob(C)
       ((cat-comp(C) (T X) (T (T X)) (T X) (M5 (T X)) (M6 X)) (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
∧ (∀X:cat-ob(C)
     ((cat-comp(C) (T X) (T (T X)) (T X) (T (T X) (M5 X)) (M6 X)) (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
∧ (∀X:cat-ob(C)
     ((cat-comp(C) (T (T (T X))) (T (T X)) (T X) (M6 (T X)) (M6 X))
     (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (T X) (M6 X)) (M6 X))
     ∈ (cat-arrow(C) (T (T (T X))) (T X))))
11. T1 T ∈ Functor(C;C)
12. ∀x:cat-ob(C). ((T1 x) (T x) ∈ cat-ob(C))
13. ∀x:cat-ob(C). ((M7 x) (M5 x) ∈ (cat-arrow(C) (T1 x)))
14. ∀x:cat-ob(C). ((M8 x) (M6 x) ∈ (cat-arrow(C) (T1 (T1 x)) (T1 x)))
⊢ M7 M5 ∈ (A:cat-ob(C) ⟶ (cat-arrow(C) (1 A) (T1 A)))
BY
(RepUR ``id_functor`` THEN FunExt THEN Auto) }


Latex:


Latex:

1.  C  :  SmallCategory
2.  T1  :  Functor(C;C)
3.  M7  :  A:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(C)  (1  A)  (T1  A))
4.  \mforall{}A,B:cat-ob(C).  \mforall{}g:cat-arrow(C)  A  B.
          ((cat-comp(C)  (1  A)  (T1  A)  (T1  B)  (M7  A)  (T1  A  B  g))
          =  (cat-comp(C)  (1  A)  (1  B)  (T1  B)  (1  A  B  g)  (M7  B)))
5.  M8  :  nat-trans(C;C;functor-comp(T1;T1);T1)
6.  (\mforall{}X:cat-ob(C).  ((cat-comp(C)  (T1  X)  (T1  (T1  X))  (T1  X)  (M7  (T1  X))  (M8  X))  =  (cat-id(C)  (T1  X))))
\mwedge{}  (\mforall{}X:cat-ob(C)
          ((cat-comp(C)  (T1  X)  (T1  (T1  X))  (T1  X)  (T1  X  (T1  X)  (M7  X))  (M8  X))  =  (cat-id(C)  (T1  X))))
\mwedge{}  (\mforall{}X:cat-ob(C)
          ((cat-comp(C)  (T1  (T1  (T1  X)))  (T1  (T1  X))  (T1  X)  (M8  (T1  X))  (M8  X))
          =  (cat-comp(C)  (T1  (T1  (T1  X)))  (T1  (T1  X))  (T1  X)  (T1  (T1  (T1  X))  (T1  X)  (M8  X))  (M8  X))))
7.  T  :  Functor(C;C)
8.  M5  :  nat-trans(C;C;1;T)
9.  M6  :  nat-trans(C;C;functor-comp(T;T);T)
10.  (\mforall{}X:cat-ob(C).  ((cat-comp(C)  (T  X)  (T  (T  X))  (T  X)  (M5  (T  X))  (M6  X))  =  (cat-id(C)  (T  X))))
\mwedge{}  (\mforall{}X:cat-ob(C)
          ((cat-comp(C)  (T  X)  (T  (T  X))  (T  X)  (T  X  (T  X)  (M5  X))  (M6  X))  =  (cat-id(C)  (T  X))))
\mwedge{}  (\mforall{}X:cat-ob(C)
          ((cat-comp(C)  (T  (T  (T  X)))  (T  (T  X))  (T  X)  (M6  (T  X))  (M6  X))
          =  (cat-comp(C)  (T  (T  (T  X)))  (T  (T  X))  (T  X)  (T  (T  (T  X))  (T  X)  (M6  X))  (M6  X))))
11.  T1  =  T
12.  \mforall{}x:cat-ob(C).  ((T1  x)  =  (T  x))
13.  \mforall{}x:cat-ob(C).  ((M7  x)  =  (M5  x))
14.  \mforall{}x:cat-ob(C).  ((M8  x)  =  (M6  x))
\mvdash{}  M7  =  M5


By


Latex:
(RepUR  ``id\_functor``  0  THEN  FunExt  THEN  Auto)




Home Index