From 63a51fbfdc16bcc96db848bddccfe41fee972400 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 16:08:37 +0100 Subject: [PATCH] Include modules in "everything"-module --- src/Cat.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Cat.agda b/src/Cat.agda index 86e6879..80d101d 100644 --- a/src/Cat.agda +++ b/src/Cat.agda @@ -8,7 +8,10 @@ open import Cat.Category.Exponential open import Cat.Category.CartesianClosed open import Cat.Category.NaturalTransformation open import Cat.Category.Yoneda +open import Cat.Category.Monoid open import Cat.Category.Monad +open Cat.Category.Monad.Monoidal +open Cat.Category.Monad.Kleisli open import Cat.Category.Monad.Voevodsky open import Cat.Categories.Sets