| Copyright | Guillaume Sabbagh 2022 |
|---|---|
| License | GPL-3 |
| Maintainer | guillaumesabbagh@protonmail.com |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Math.FiniteCategories.ExponentialCategory
Description
(FinCat ExponentialCategory) is the category in which live the exponential objects of FinCat with the original categories. To compute exponential objects in a usual category, see Math.CartesianClosedCategory. To compute exponential objects in a custom FiniteCategory, see exponentialObjects in Math.CartesianClosedCategory.
Synopsis
- data ExponentialCategoryObject c m o
- = ExprojectedObject o
- | ExponentialElementObject (FinFunctor c m o)
- data ExponentialCategoryMorphism c m o
- = ExprojectedMorphism m
- | ExponentialElementMorphism (NaturalTransformation c m o c m o)
- data ExponentialCategory c m o
- = ExprojectedCategory c
- | ExponentialCategory (FunctorCategory c m o c m o)
- type CartesianObject c m o = TwoProductOfCategoriesObject (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o)
- type CartesianMorphism c m o = TwoProductOfCategoriesMorphism (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o)
- type CartesianCategory c m o = TwoProductOfCategories (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o)
Exponential category
Object
data ExponentialCategoryObject c m o Source #
An object in an ExponentialCategory. It is either a ExprojectedObject in an original category or a ExponentialElementObject.
Constructors
| ExprojectedObject o | An |
| ExponentialElementObject (FinFunctor c m o) | The exponential elemets in Cat are functors. |
Instances
Morphism
data ExponentialCategoryMorphism c m o Source #
A morphism in an ExponentialCategory. It is either a ExprojectedMorphism in an original category or an ExponentialElementMorphism.
Constructors
| ExprojectedMorphism m | An |
| ExponentialElementMorphism (NaturalTransformation c m o c m o) | A |
Instances
Category
data ExponentialCategory c m o Source #
An ExponentialCategory is either an ExprojectedCategory (an original category) or an ExponentialCategory.
Constructors
| ExprojectedCategory c | An original category in |
| ExponentialCategory (FunctorCategory c m o c m o) | The exponential category of a given 2-base is a |
Instances
Cartesian category type
Object
type CartesianObject c m o = TwoProductOfCategoriesObject (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) Source #
An object in CartesianCategory.
Morphism
type CartesianMorphism c m o = TwoProductOfCategoriesMorphism (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) Source #
A morphism in CartesianCategory.
Category
type CartesianCategory c m o = TwoProductOfCategories (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) Source #
The type of the category containing categories and their exponential objects.