Monoidal monads are also groupoids

2018-05-22 16:28:23 +02:00 · 2018-05-22 16:28:23 +02:00 · cb0117819b
parent b116247702
commit cb0117819b
1 changed files with 7 additions and 0 deletions
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@ -231,3 +231,10 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where

  Monoidal≡Kleisli : Monoidal.Monad ≡ Kleisli.Monad
  Monoidal≡Kleisli = isoToPath Monoidal≊Kleisli
+
+  grpdKleisli : isGrpd Kleisli.Monad
+  grpdKleisli = Kleisli.grpdMonad
+
+  grpdMonoidal : isGrpd Monoidal.Monad
+  grpdMonoidal = subst {P = isGrpd}
+    (sym Monoidal≡Kleisli) grpdKleisli