Include modules in "everything"-module

This commit is contained in:
Frederik Hanghøj Iversen 2018-03-20 16:08:37 +01:00
parent 811a6bf58e
commit 63a51fbfdc

View file

@ -8,7 +8,10 @@ open import Cat.Category.Exponential
open import Cat.Category.CartesianClosed open import Cat.Category.CartesianClosed
open import Cat.Category.NaturalTransformation open import Cat.Category.NaturalTransformation
open import Cat.Category.Yoneda open import Cat.Category.Yoneda
open import Cat.Category.Monoid
open import Cat.Category.Monad open import Cat.Category.Monad
open Cat.Category.Monad.Monoidal
open Cat.Category.Monad.Kleisli
open import Cat.Category.Monad.Voevodsky open import Cat.Category.Monad.Voevodsky
open import Cat.Categories.Sets open import Cat.Categories.Sets