---

Step * of Lemma monad-equations

∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x:cat-ob(C)].
  ((((cat-comp(C) M(x) M(M(x)) M(x) monad-unit(M;M(x)) monad-op(M;x)) = (cat-id(C) M(x)) ∈ (cat-arrow(C) M(x) M(x)))
  ∧ ((cat-comp(C) M(x) M(M(x)) M(x) (arrow(monad-functor(M)) x M(x) monad-unit(M;x)) monad-op(M;x))
    = (cat-id(C) M(x))
    ∈ (cat-arrow(C) M(x) M(x))))
  ∧ ((cat-comp(C) M(M(M(x))) M(M(x)) M(x) monad-op(M;M(x)) monad-op(M;x))
    = (cat-comp(C) M(M(M(x))) M(M(x)) M(x) (arrow(monad-functor(M)) M(M(x)) M(x) monad-op(M;x)) monad-op(M;x))
    ∈ (cat-arrow(C) M(M(M(x))) M(x))))
BY
{ (Auto
   THEN (D 2 THEN DProds THEN All Reduce⋅ THEN ExRepD)
   THEN RepUR ``monad-fun monad-functor monad-unit monad-op`` 0
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[M:Monad(C)].  \mforall{}[x:cat-ob(C)].
    ((((cat-comp(C)  M(x)  M(M(x))  M(x)  monad-unit(M;M(x))  monad-op(M;x))  =  (cat-id(C)  M(x)))
    \mwedge{}  ((cat-comp(C)  M(x)  M(M(x))  M(x)  (arrow(monad-functor(M))  x  M(x)  monad-unit(M;x))  monad-op(M;x))
        =  (cat-id(C)  M(x))))
    \mwedge{}  ((cat-comp(C)  M(M(M(x)))  M(M(x))  M(x)  monad-op(M;M(x))  monad-op(M;x))
        =  (cat-comp(C)  M(M(M(x)))  M(M(x))  M(x)  (arrow(monad-functor(M))  M(M(x))  M(x)  monad-op(M;x)) 
              monad-op(M;x))))


By

---

Latex:
(Auto
  THEN  (D  2  THEN  DProds  THEN  All  Reduce\mcdot{}  THEN  ExRepD)
  THEN  RepUR  ``monad-fun  monad-functor  monad-unit  monad-op``  0
  THEN  BackThruSomeHyp)

---

Home Index