---

Step * 1 of Lemma equal-monads


1. C : SmallCategory
2. M1 : T:Functor(C;C) × nat-trans(C;C;1;T) × nat-trans(C;C;functor-comp(T;T);T)
3. let T,u,m = M1 in 
(∀X:cat-ob(C). ((cat-comp(C) (T X) (T (T X)) (T X) (u (T X)) (m 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 X (T X) (u X)) (m 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) (m (T X)) (m X))
     = (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (T X) (m X)) (m X))
     ∈ (cat-arrow(C) (T (T (T X))) (T X))))
4. M2 : Monad(C)
5. monad-functor(M1) = monad-functor(M2) ∈ Functor(C;C)
6. ∀x:cat-ob(C). (M1(x) = M2(x) ∈ cat-ob(C))
7. ∀x:cat-ob(C). (monad-unit(M1;x) = monad-unit(M2;x) ∈ (cat-arrow(C) x M1(x)))
8. ∀x:cat-ob(C). (monad-op(M1;x) = monad-op(M2;x) ∈ (cat-arrow(C) M1(M1(x)) M1(x)))
⊢ M1 = M2 ∈ (T:Functor(C;C) × nat-trans(C;C;1;T) × nat-trans(C;C;functor-comp(T;T);T))
BY
{ (DVar `M2'
   THEN DProds
   THEN (All Reduce THEN All (RepUR ``monad-functor monad-unit monad-fun monad-op``))
   THEN EqCDA
   THEN Try (Trivial)
   THEN EqCDA) }

1
.....subterm..... T:t
1:n
1. C : SmallCategory
2. T1 : Functor(C;C)
3. M7 : nat-trans(C;C;1;T1)
4. M8 : nat-trans(C;C;functor-comp(T1;T1);T1)
5. (∀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 X (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))))
6. T : Functor(C;C)
7. M5 : nat-trans(C;C;1;T)
8. M6 : nat-trans(C;C;functor-comp(T;T);T)
9. (∀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 X (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))))
10. T1 = T ∈ Functor(C;C)
11. ∀x:cat-ob(C). ((T1 x) = (T x) ∈ cat-ob(C))
12. ∀x:cat-ob(C). ((M7 x) = (M5 x) ∈ (cat-arrow(C) x (T1 x)))
13. ∀x:cat-ob(C). ((M8 x) = (M6 x) ∈ (cat-arrow(C) (T1 (T1 x)) (T1 x)))
⊢ M7 = M5 ∈ nat-trans(C;C;1;T1)

2
.....subterm..... T:t
2:n
1. C : SmallCategory
2. T1 : Functor(C;C)
3. M7 : nat-trans(C;C;1;T1)
4. M8 : nat-trans(C;C;functor-comp(T1;T1);T1)
5. (∀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 X (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))))
6. T : Functor(C;C)
7. M5 : nat-trans(C;C;1;T)
8. M6 : nat-trans(C;C;functor-comp(T;T);T)
9. (∀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 X (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))))
10. T1 = T ∈ Functor(C;C)
11. ∀x:cat-ob(C). ((T1 x) = (T x) ∈ cat-ob(C))
12. ∀x:cat-ob(C). ((M7 x) = (M5 x) ∈ (cat-arrow(C) x (T1 x)))
13. ∀x:cat-ob(C). ((M8 x) = (M6 x) ∈ (cat-arrow(C) (T1 (T1 x)) (T1 x)))
⊢ M8 = M6 ∈ nat-trans(C;C;functor-comp(T1;T1);T1)

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  M1  :  T:Functor(C;C)  \mtimes{}  nat-trans(C;C;1;T)  \mtimes{}  nat-trans(C;C;functor-comp(T;T);T)
3.  let  T,u,m  =  M1  in 
(\mforall{}X:cat-ob(C).  ((cat-comp(C)  (T  X)  (T  (T  X))  (T  X)  (u  (T  X))  (m  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)  (u  X))  (m  X))  =  (cat-id(C)  (T  X))))
\mwedge{}  (\mforall{}X:cat-ob(C)
          ((cat-comp(C)  (T  (T  (T  X)))  (T  (T  X))  (T  X)  (m  (T  X))  (m  X))
          =  (cat-comp(C)  (T  (T  (T  X)))  (T  (T  X))  (T  X)  (T  (T  (T  X))  (T  X)  (m  X))  (m  X))))
4.  M2  :  Monad(C)
5.  monad-functor(M1)  =  monad-functor(M2)
6.  \mforall{}x:cat-ob(C).  (M1(x)  =  M2(x))
7.  \mforall{}x:cat-ob(C).  (monad-unit(M1;x)  =  monad-unit(M2;x))
8.  \mforall{}x:cat-ob(C).  (monad-op(M1;x)  =  monad-op(M2;x))
\mvdash{}  M1  =  M2


By

---

Latex:
(DVar  `M2'
  THEN  DProds
  THEN  (All  Reduce  THEN  All  (RepUR  ``monad-functor  monad-unit  monad-fun  monad-op``))
  THEN  EqCDA
  THEN  Try  (Trivial)
  THEN  EqCDA)

---

Home Index