From 7aec22b30af72dd645298b6134af0579cc9c2702 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 14 Mar 2018 11:00:52 +0100 Subject: [PATCH] Expose both monad formulations qualified from Cat.Category.Monad --- src/Cat/Category/Monad.agda | 7 +++++-- src/Cat/Category/Monad/Voevodsky.agda | 4 +--- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 2f42f32..7f8637a 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -31,10 +31,13 @@ open import Cubical.GradLemma using (gradLemma) open import Cat.Category open import Cat.Category.Functor as F open import Cat.Category.NaturalTransformation -open import Cat.Category.Monad.Monoidal as Monoidal public -open import Cat.Category.Monad.Kleisli as Kleisli +import Cat.Category.Monad.Monoidal +import Cat.Category.Monad.Kleisli open import Cat.Categories.Fun +module Monoidal = Cat.Category.Monad.Monoidal +module Kleisli = Cat.Category.Monad.Kleisli + -- | The monoidal- and kleisli presentation of monads are equivalent. module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where private diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda index d64d3f7..4409039 100644 --- a/src/Cat/Category/Monad/Voevodsky.agda +++ b/src/Cat/Category/Monad/Voevodsky.agda @@ -16,9 +16,7 @@ open import Cubical.GradLemma using (gradLemma) open import Cat.Category open import Cat.Category.Functor as F open import Cat.Category.NaturalTransformation -open import Cat.Category.Monad using (Monoidal≃Kleisli) -import Cat.Category.Monad.Monoidal as Monoidal -import Cat.Category.Monad.Kleisli as Kleisli +open import Cat.Category.Monad open import Cat.Categories.Fun -- Utilities