---

Step * of Lemma equal-monads

∀[C:SmallCategory]. ∀[M1,M2:Monad(C)].
  (M1 = M2 ∈ Monad(C)) supposing 
     ((∀x:cat-ob(C). (monad-op(M1;x) = monad-op(M2;x) ∈ (cat-arrow(C) M1(M1(x)) M1(x)))) and 
     (∀x:cat-ob(C). (monad-unit(M1;x) = monad-unit(M2;x) ∈ (cat-arrow(C) x M1(x)))) and 
     (monad-functor(M1) = monad-functor(M2) ∈ Functor(C;C)))
BY
{ (RepeatFor 4 (Intro)
   THEN (Assert ⌜∀x:cat-ob(C). (M1(x) = M2(x) ∈ cat-ob(C))⌝⋅ THENA (RepUR ``monad-fun`` 0 THEN Auto))
   THEN Intros
   THEN DVar `M1'
   THEN At ⌜Type⌝ EqTypeCD⋅
   THEN Try (Trivial)
   THEN Try (((RepeatFor 2 (D -1) THEN Reduce 0)
              THEN (D -2 THEN D -1 THEN All (RepUR  ``functor-comp id_functor``))
              THEN Auto))) }

1
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))

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[M1,M2:Monad(C)].
    (M1  =  M2)  supposing 
          ((\mforall{}x:cat-ob(C).  (monad-op(M1;x)  =  monad-op(M2;x)))  and 
          (\mforall{}x:cat-ob(C).  (monad-unit(M1;x)  =  monad-unit(M2;x)))  and 
          (monad-functor(M1)  =  monad-functor(M2)))


By

---

Latex:
(RepeatFor  4  (Intro)
  THEN  (Assert  \mkleeneopen{}\mforall{}x:cat-ob(C).  (M1(x)  =  M2(x))\mkleeneclose{}\mcdot{}  THENA  (RepUR  ``monad-fun``  0  THEN  Auto))
  THEN  Intros
  THEN  DVar  `M1'
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  EqTypeCD\mcdot{}
  THEN  Try  (Trivial)
  THEN  Try  (((RepeatFor  2  (D  -1)  THEN  Reduce  0)
                        THEN  (D  -2  THEN  D  -1  THEN  All  (RepUR    ``functor-comp  id\_functor``))
                        THEN  Auto)))

---

Home Index