2018-01-20 23:21:51 +00:00
|
|
|
module Cat where
|
|
|
|
|
|
2018-03-05 09:28:16 +00:00
|
|
|
open import Cat.Category
|
2018-02-05 13:08:30 +00:00
|
|
|
|
2018-03-05 09:28:16 +00:00
|
|
|
open import Cat.Category.Functor
|
|
|
|
|
open import Cat.Category.Product
|
|
|
|
|
open import Cat.Category.Exponential
|
|
|
|
|
open import Cat.Category.CartesianClosed
|
|
|
|
|
open import Cat.Category.NaturalTransformation
|
|
|
|
|
open import Cat.Category.Yoneda
|
2018-03-20 15:08:37 +00:00
|
|
|
open import Cat.Category.Monoid
|
2018-03-05 09:28:16 +00:00
|
|
|
open import Cat.Category.Monad
|
2018-05-11 11:20:03 +00:00
|
|
|
open import Cat.Category.Monad.Monoidal
|
|
|
|
|
open import Cat.Category.Monad.Kleisli
|
2018-03-12 13:04:10 +00:00
|
|
|
open import Cat.Category.Monad.Voevodsky
|
2018-02-05 13:08:30 +00:00
|
|
|
|
2018-05-15 14:28:04 +00:00
|
|
|
open import Cat.Categories.Opposite
|
2018-03-05 09:28:16 +00:00
|
|
|
open import Cat.Categories.Sets
|
|
|
|
|
open import Cat.Categories.Cat
|
|
|
|
|
open import Cat.Categories.Rel
|
|
|
|
|
open import Cat.Categories.Free
|
|
|
|
|
open import Cat.Categories.Fun
|
2018-10-30 13:37:15 +00:00
|
|
|
-- open import Cat.Categories.Cube
|
2018-03-05 09:28:16 +00:00
|
|
|
open import Cat.Categories.CwF
|
