FiniteCategories-0.6.4.0: Finite categories and usual categorical constructions on them.
CopyrightGuillaume Sabbagh 2022
LicenseGPL-3
Maintainerguillaumesabbagh@protonmail.com
Stabilityexperimental
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

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 ExprojectedObject is an object o.

ExponentialElementObject (FinFunctor c m o)

The exponential elemets in Cat are functors.

Instances

Instances details
(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) => PrettyPrint (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

pprint :: Int -> ExponentialCategoryObject c m o -> String Source #

pprintWithIndentations :: Int -> Int -> String -> ExponentialCategoryObject c m o -> String Source #

pprintIndent :: Int -> ExponentialCategoryObject c m o -> String Source #

(Simplifiable o, Simplifiable c, Simplifiable m, Eq o, Eq m) => Simplifiable (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

simplify :: ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o #

Generic (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Associated Types

type Rep (ExponentialCategoryObject c m o) :: Type -> Type

Methods

from :: ExponentialCategoryObject c m o -> Rep (ExponentialCategoryObject c m o) x

to :: Rep (ExponentialCategoryObject c m o) x -> ExponentialCategoryObject c m o

(Show o, Show c, Show m) => Show (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

showsPrec :: Int -> ExponentialCategoryObject c m o -> ShowS

show :: ExponentialCategoryObject c m o -> String

showList :: [ExponentialCategoryObject c m o] -> ShowS

(Eq o, Eq c, Eq m, FiniteCategory c m o, Morphism m o) => Eq (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

(==) :: ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o -> Bool

(/=) :: ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o -> Bool

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Morphism (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

(@) :: ExponentialCategoryMorphism c m o -> ExponentialCategoryMorphism c m o -> ExponentialCategoryMorphism c m o Source #

(@?) :: ExponentialCategoryMorphism c m o -> ExponentialCategoryMorphism c m o -> Maybe (ExponentialCategoryMorphism c m o) Source #

source :: ExponentialCategoryMorphism c m o -> ExponentialCategoryObject c m o Source #

target :: ExponentialCategoryMorphism c m o -> ExponentialCategoryObject c m o Source #

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Category (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

identity :: ExponentialCategory c m o -> ExponentialCategoryObject c m o -> ExponentialCategoryMorphism c m o Source #

ar :: ExponentialCategory c m o -> ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o -> Set (ExponentialCategoryMorphism c m o) Source #

genAr :: ExponentialCategory c m o -> ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o -> Set (ExponentialCategoryMorphism c m o) Source #

decompose :: ExponentialCategory c m o -> ExponentialCategoryMorphism c m o -> [ExponentialCategoryMorphism c m o] Source #

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

ob :: ExponentialCategory c m o -> Set (ExponentialCategoryObject c m o) Source #

type Rep (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

type Rep (ExponentialCategoryObject c m o) = D1 ('MetaData "ExponentialCategoryObject" "Math.FiniteCategories.ExponentialCategory" "FiniteCategories-0.6.4.0-inplace" 'False) (C1 ('MetaCons "ExprojectedObject" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 o)) :+: C1 ('MetaCons "ExponentialElementObject" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FinFunctor c m o))))

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 ExprojectedMorphism is a morphism m.

ExponentialElementMorphism (NaturalTransformation c m o c m o)

A NaturalTransformation is a morphism in the ExponentialCategory.

Instances

Instances details
(PrettyPrint m, PrettyPrint c, PrettyPrint o, Eq o, Eq m) => PrettyPrint (ExponentialCategoryMorphism c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

pprint :: Int -> ExponentialCategoryMorphism c m o -> String Source #

pprintWithIndentations :: Int -> Int -> String -> ExponentialCategoryMorphism c m o -> String Source #

pprintIndent :: Int -> ExponentialCategoryMorphism c m o -> String Source #

(Simplifiable m, Simplifiable c, Simplifiable o, Eq o, Eq m) => Simplifiable (ExponentialCategoryMorphism c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

simplify :: ExponentialCategoryMorphism c m o -> ExponentialCategoryMorphism c m o #

Generic (ExponentialCategoryMorphism c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Associated Types

type Rep (ExponentialCategoryMorphism c m o) :: Type -> Type

Methods

from :: ExponentialCategoryMorphism c m o -> Rep (ExponentialCategoryMorphism c m o) x

to :: Rep (ExponentialCategoryMorphism c m o) x -> ExponentialCategoryMorphism c m o

(Show m, Show c, Show o) => Show (ExponentialCategoryMorphism c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

showsPrec :: Int -> ExponentialCategoryMorphism c m o -> ShowS

show :: ExponentialCategoryMorphism c m o -> String

showList :: [ExponentialCategoryMorphism c m o] -> ShowS

(Eq m, Eq c, Eq o, FiniteCategory c m o, Morphism m o) => Eq (ExponentialCategoryMorphism c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

(==) :: ExponentialCategoryMorphism c m o -> ExponentialCategoryMorphism c m o -> Bool

(/=) :: ExponentialCategoryMorphism c m o -> ExponentialCategoryMorphism c m o -> Bool

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Morphism (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

(@) :: ExponentialCategoryMorphism c m o -> ExponentialCategoryMorphism c m o -> ExponentialCategoryMorphism c m o Source #

(@?) :: ExponentialCategoryMorphism c m o -> ExponentialCategoryMorphism c m o -> Maybe (ExponentialCategoryMorphism c m o) Source #

source :: ExponentialCategoryMorphism c m o -> ExponentialCategoryObject c m o Source #

target :: ExponentialCategoryMorphism c m o -> ExponentialCategoryObject c m o Source #

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Category (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

identity :: ExponentialCategory c m o -> ExponentialCategoryObject c m o -> ExponentialCategoryMorphism c m o Source #

ar :: ExponentialCategory c m o -> ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o -> Set (ExponentialCategoryMorphism c m o) Source #

genAr :: ExponentialCategory c m o -> ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o -> Set (ExponentialCategoryMorphism c m o) Source #

decompose :: ExponentialCategory c m o -> ExponentialCategoryMorphism c m o -> [ExponentialCategoryMorphism c m o] Source #

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

ob :: ExponentialCategory c m o -> Set (ExponentialCategoryObject c m o) Source #

type Rep (ExponentialCategoryMorphism c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

type Rep (ExponentialCategoryMorphism c m o) = D1 ('MetaData "ExponentialCategoryMorphism" "Math.FiniteCategories.ExponentialCategory" "FiniteCategories-0.6.4.0-inplace" 'False) (C1 ('MetaCons "ExprojectedMorphism" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 m)) :+: C1 ('MetaCons "ExponentialElementMorphism" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NaturalTransformation c m o c m o))))

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 FinCat.

ExponentialCategory (FunctorCategory c m o c m o)

The exponential category of a given 2-base is a FunctorCategory.

Instances

Instances details
PrettyPrint c => PrettyPrint (ExponentialCategory c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

pprint :: Int -> ExponentialCategory c m o -> String Source #

pprintWithIndentations :: Int -> Int -> String -> ExponentialCategory c m o -> String Source #

pprintIndent :: Int -> ExponentialCategory c m o -> String Source #

Simplifiable c => Simplifiable (ExponentialCategory c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

simplify :: ExponentialCategory c m o -> ExponentialCategory c m o #

Generic (ExponentialCategory c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Associated Types

type Rep (ExponentialCategory c m o) :: Type -> Type

Methods

from :: ExponentialCategory c m o -> Rep (ExponentialCategory c m o) x

to :: Rep (ExponentialCategory c m o) x -> ExponentialCategory c m o

Show c => Show (ExponentialCategory c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

showsPrec :: Int -> ExponentialCategory c m o -> ShowS

show :: ExponentialCategory c m o -> String

showList :: [ExponentialCategory c m o] -> ShowS

Eq c => Eq (ExponentialCategory c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

(==) :: ExponentialCategory c m o -> ExponentialCategory c m o -> Bool

(/=) :: ExponentialCategory c m o -> ExponentialCategory c m o -> Bool

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Category (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

identity :: ExponentialCategory c m o -> ExponentialCategoryObject c m o -> ExponentialCategoryMorphism c m o Source #

ar :: ExponentialCategory c m o -> ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o -> Set (ExponentialCategoryMorphism c m o) Source #

genAr :: ExponentialCategory c m o -> ExponentialCategoryObject c m o -> ExponentialCategoryObject c m o -> Set (ExponentialCategoryMorphism c m o) Source #

decompose :: ExponentialCategory c m o -> ExponentialCategoryMorphism c m o -> [ExponentialCategoryMorphism c m o] Source #

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (ExponentialCategory c m o) (ExponentialCategoryMorphism c m o) (ExponentialCategoryObject c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

Methods

ob :: ExponentialCategory c m o -> Set (ExponentialCategoryObject c m o) Source #

type Rep (ExponentialCategory c m o) Source # 
Instance details

Defined in Math.FiniteCategories.ExponentialCategory

type Rep (ExponentialCategory c m o) = D1 ('MetaData "ExponentialCategory" "Math.FiniteCategories.ExponentialCategory" "FiniteCategories-0.6.4.0-inplace" 'False) (C1 ('MetaCons "ExprojectedCategory" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 c)) :+: C1 ('MetaCons "ExponentialCategory" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FunctorCategory c m o c m o))))

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.