From Categories Require Export Cat.Initial.
From Categories Require Export Cat.Terminal.
From Categories Require Export Cat.Product.
From Categories Require Export Cat.Exponential.
From Categories Require Export Cat.CCC.
