25 lines
710 B
Agda
25 lines
710 B
Agda
module Cat where
|
|
|
|
open import Cat.Category
|
|
|
|
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
|
|
open import Cat.Category.Monoid
|
|
open import Cat.Category.Monad
|
|
open import Cat.Category.Monad.Monoidal
|
|
open import Cat.Category.Monad.Kleisli
|
|
open import Cat.Category.Monad.Voevodsky
|
|
|
|
open import Cat.Categories.Opposite
|
|
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
|
|
-- open import Cat.Categories.Cube
|
|
open import Cat.Categories.CwF
|