---

Step * of Lemma monad-extend-unit

∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[y:cat-ob(C)].
  (monad-extend(C;M;y;y;monad-unit(M;y)) = (cat-id(C) M(y)) ∈ (cat-arrow(C) M(y) M(y)))
BY
{ (Auto
   THEN DVar `M'
   THEN DProds
   THEN DVar `M2'
   THEN DVar `M3'
   THEN (All (RepUR ``id_functor functor-comp monad-extend monad-fun``)
         THEN All (RepUR ``monad-functor monad-unit monad-op``)
         )
   THEN All Reduce
   THEN ExRepD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[M:Monad(C)].  \mforall{}[y:cat-ob(C)].
    (monad-extend(C;M;y;y;monad-unit(M;y))  =  (cat-id(C)  M(y)))


By

---

Latex:
(Auto
  THEN  DVar  `M'
  THEN  DProds
  THEN  DVar  `M2'
  THEN  DVar  `M3'
  THEN  (All  (RepUR  ``id\_functor  functor-comp  monad-extend  monad-fun``)
              THEN  All  (RepUR  ``monad-functor  monad-unit  monad-op``)
              )
  THEN  All  Reduce
  THEN  ExRepD
  THEN  Auto)

---

Home Index