Copyright | Guillaume Sabbagh 2022 |
---|---|
License | GPL-3 |
Maintainer | guillaumesabbagh@protonmail.com |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
(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
.
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
.
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
.
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.