---

Step * of Lemma mk-monad_wf

∀[C:SmallCategory]. ∀[T:Functor(C;C)]. ∀[u:nat-trans(C;C;1;T)]. ∀[m:nat-trans(C;C;functor-comp(T;T);T)].
  (mk-monad(T;u;m) ∈ Monad(C)) supposing 
     ((∀X:cat-ob(C)
         ((cat-comp(C) (ob(T) X) (ob(T) (ob(T) X)) (ob(T) X) (u (ob(T) X)) (m X))
         = (cat-id(C) (ob(T) X))
         ∈ (cat-arrow(C) (ob(T) X) (ob(T) X)))) and 
     (∀X:cat-ob(C)
        ((cat-comp(C) (ob(T) X) (ob(T) (ob(T) X)) (ob(T) X) (arrow(T) X (ob(T) X) (u X)) (m X))
        = (cat-id(C) (ob(T) X))
        ∈ (cat-arrow(C) (ob(T) X) (ob(T) X)))) and 
     (∀X:cat-ob(C)
        ((cat-comp(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) (ob(T) X)) (ob(T) X) (m (ob(T) X)) (m 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) (m X)) 
           (m X))
        ∈ (cat-arrow(C) (ob(T) (ob(T) (ob(T) X))) (ob(T) X)))))
BY
{ (RepeatFor 4 (Intro)
   THEN All (RepUR ``nat-trans id_functor functor-comp``)
   THEN Intros
   THEN (At ⌜Type⌝ MemTypeCD⋅
         THENW ((RepeatFor 2 (D -1) THEN Reduce 0)
                THEN (D -2 THEN D -1 THEN All (RepUR  ``functor-comp id_functor``))
                THEN Auto)
         )
   THEN All (RepUR ``mk-monad nat-trans id_functor functor-comp``)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[T:Functor(C;C)].  \mforall{}[u:nat-trans(C;C;1;T)].
\mforall{}[m:nat-trans(C;C;functor-comp(T;T);T)].
    (mk-monad(T;u;m)  \mmember{}  Monad(C))  supposing 
          ((\mforall{}X:cat-ob(C)
                  ((cat-comp(C)  (ob(T)  X)  (ob(T)  (ob(T)  X))  (ob(T)  X)  (u  (ob(T)  X))  (m  X))
                  =  (cat-id(C)  (ob(T)  X))))  and 
          (\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)  (u  X))  (m  X))
                =  (cat-id(C)  (ob(T)  X))))  and 
          (\mforall{}X:cat-ob(C)
                ((cat-comp(C)  (ob(T)  (ob(T)  (ob(T)  X)))  (ob(T)  (ob(T)  X))  (ob(T)  X)  (m  (ob(T)  X))  (m  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)  (m  X)) 
                      (m  X)))))


By

---

Latex:
(RepeatFor  4  (Intro)
  THEN  All  (RepUR  ``nat-trans  id\_functor  functor-comp``)
  THEN  Intros
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{}
              THENW  ((RepeatFor  2  (D  -1)  THEN  Reduce  0)
                            THEN  (D  -2  THEN  D  -1  THEN  All  (RepUR    ``functor-comp  id\_functor``))
                            THEN  Auto)
              )
  THEN  All  (RepUR  ``mk-monad  nat-trans  id\_functor  functor-comp``)
  THEN  Auto)

---

Home Index