Math.CartesianClosedCategory

Typeclasses for Category which are cartesian complete.

A TwoBase specifies an internal domain and an internal codomain.

A Tripod is the data necessary to specify an exponential object.

An exponential object is a terminal object in the category of candidate exponential objects.

2-base

type TwoBase c m o = Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o

A TwoBase is the specification of an internal domain and an internal codomain.

The object A selects the internal domain, the object B selects the internal codomain.

Don't confuse the 2-base of an exponential object with the base of its 2-cone. The 2-base selects the internal domain and internal codomain of the exponential object. The base of the 2-cone selects the power object and the internal domain.

Tripod

data Tripod c m o

A Tripod is a 2-cone on the power object and the internal domain, and an evaluation map from the apex of the 2-cone to the internal codomain.

Tripod is private, use smart constructor tripod which checks the structure of the Tripod or use unsafeTripod if you know that the evalMap has the apex of the twoCone as a source.

Instances

(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) => PrettyPrint (Tripod c m o)

Defined in Math.CartesianClosedCategory

Methods

pprint :: Int -> Tripod c m o -> String

pprintWithIndentations :: Int -> Int -> String -> Tripod c m o -> String

pprintIndent :: Int -> Tripod c m o -> String

(Simplifiable o, Simplifiable c, Simplifiable m) => Simplifiable (Tripod c m o)

Defined in Math.CartesianClosedCategory

Methods

simplify :: Tripod c m o -> Tripod c m o

Generic (Tripod c m o)

Defined in Math.CartesianClosedCategory

Associated Types

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

Methods

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

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

(Show o, Show c, Show m) => Show (Tripod c m o)

Defined in Math.CartesianClosedCategory

Methods

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

show :: Tripod c m o -> String

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

(Eq o, Eq c, Eq m) => Eq (Tripod c m o)

Defined in Math.CartesianClosedCategory

Methods

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

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

Morphism m o => Morphism (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o)

Defined in Math.CartesianClosedCategory

Methods

(@) :: CandidateExponentialObjectMorphism c m o -> CandidateExponentialObjectMorphism c m o -> CandidateExponentialObjectMorphism c m o

(@?) :: CandidateExponentialObjectMorphism c m o -> CandidateExponentialObjectMorphism c m o -> Maybe (CandidateExponentialObjectMorphism c m o)

source :: CandidateExponentialObjectMorphism c m o -> CandidateExponentialObject c m o

target :: CandidateExponentialObjectMorphism c m o -> CandidateExponentialObject c m o

(Category c m o, Morphism m o, Eq c, Eq m, Eq o) => Category (CandidateExponentialObjectCategory c m o) (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o)

Defined in Math.CartesianClosedCategory

Methods

identity :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObject c m o -> CandidateExponentialObjectMorphism c m o

ar :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> Set (CandidateExponentialObjectMorphism c m o)

genAr :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> Set (CandidateExponentialObjectMorphism c m o)

decompose :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObjectMorphism c m o -> [CandidateExponentialObjectMorphism c m o]

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (CandidateExponentialObjectCategory c m o) (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o)

Defined in Math.CartesianClosedCategory

Methods

ob :: CandidateExponentialObjectCategory c m o -> Set (CandidateExponentialObject c m o)

type Rep (Tripod c m o)

Defined in Math.CartesianClosedCategory

type Rep (Tripod c m o) = D1 ('MetaData "Tripod" "Math.CartesianClosedCategory" "FiniteCategories-0.6.0.0-inplace" 'False) (C1 ('MetaCons "Tripod" 'PrefixI 'True) (S1 ('MetaSel ('Just "twoCone") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o)) :*: S1 ('MetaSel ('Just "evalMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 m)))

Getters

twoCone :: Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o

In the base of the cone, the power object should be the image of A and the internal domain should be the image of B.

evalMap :: Tripod c m o -> m

The evaluation map should go from the apex of the 2-cone to the internal codomain

internalDomain :: Morphism m o => Tripod c m o -> o

Return the internal domain of a Tripod.

internalCodomain :: Morphism m o => Tripod c m o -> o

Return the internal codomain of a Tripod.

powerObject :: Morphism m o => Tripod c m o -> o

Return the power object of a Tripod.

universeCategoryTripod :: (Category c m o, Morphism m o, Eq c, Eq m, Eq o) => Tripod c m o -> c

Return the category in which a Tripod lives.

Smart constructors

tripod :: (Morphism m o, Eq o) => Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o -> m -> Maybe (Tripod c m o)

Smart constructor of Tripod, checks that the apex of the twoCone is the source of the evalMap.

unsafeTripod :: Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o -> m -> Tripod c m o

Construct a Tripod without checking the sructure of the Tripod, use with caution.

Cartesian closed category

class CartesianClosedCategory c m o cLim mLim oLim cLimExp mLimExp oLimExp | c -> m, m -> o, cLim -> mLim, mLim -> oLim, cLimExp -> mLimExp, mLimExp -> oLimExp, c m o -> cLimExp where

Methods

internalHom :: CompleteCategory c m o cLim mLim oLim DiscreteTwo DiscreteTwoAr DiscreteTwoOb => TwoBase c m o -> Tripod cLimExp mLimExp oLimExp

Instances

Eq a => CartesianClosedCategory (FinSet a) (Function a) (Set a) (FinSet (TwoProduct a)) (Function (TwoProduct a)) (Set (TwoProduct a)) (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a))

Defined in Math.Categories.FinSet

Methods

internalHom :: TwoBase (FinSet a) (Function a) (Set a) -> Tripod (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a))

type TwoProduct t = Limit DiscreteTwoOb t

For a category to be cartesian closed, we need to construct 2-products.

data Exponential t

For a Category parametrized over a type t, the power object of an exponential object of a 2-base will contain ExponentialElement constructions (an exponential element is a mapping). A given mapping has as domain and codomain values Exprojections.

For example, in FinSet, let's consider the 2-base selecting {1,2} and {3,4} as internal domain and codomain. The power object of the 2-base is {{1->3,2->3},{1->3,2->4},{1->4,2->3},{1->4,2->4}}, note that it is not an object of (Finset Int) but an object of (FinSet (Set (Map Int))). The Exponential type allows to construct type (FinSet (Exponential Int)) in which we can consider the original objects with Exprojection and the new mappings with ExponentialElement. Here, instead of mappings, we can construct the type (FinSet (Set (Exponential Int))), a mapping is then (ExponentialElement (weakMap [(1,3),(2,3)])). We can construct exprojections in the same category, for example along A which will map (ExponentialElement (weakMap [(1,3),(2,3)])) to (set [Exprojection 1, Exprojection 2]).

Constructors

Exprojection t

A ExponentialElement can be applied to an Exprojection yielding another Exprojection.

ExponentialElement (Map t t)

An ExponentialElement is an element in an exponential object, it is a mapping between objects of type t.

Instances

(PrettyPrint t, Eq t) => PrettyPrint (Exponential t)

Defined in Math.CartesianClosedCategory

Methods

pprint :: Int -> Exponential t -> String

pprintWithIndentations :: Int -> Int -> String -> Exponential t -> String

pprintIndent :: Int -> Exponential t -> String

(Simplifiable t, Eq t) => Simplifiable (Exponential t)

Defined in Math.CartesianClosedCategory

Methods

simplify :: Exponential t -> Exponential t

Generic (Exponential t)

Defined in Math.CartesianClosedCategory

Associated Types

type Rep (Exponential t) :: Type -> Type

Methods

from :: Exponential t -> Rep (Exponential t) x

to :: Rep (Exponential t) x -> Exponential t

Show t => Show (Exponential t)

Defined in Math.CartesianClosedCategory

Methods

showsPrec :: Int -> Exponential t -> ShowS

show :: Exponential t -> String

showList :: [Exponential t] -> ShowS

Eq t => Eq (Exponential t)

Defined in Math.CartesianClosedCategory

Methods

(==) :: Exponential t -> Exponential t -> Bool

(/=) :: Exponential t -> Exponential t -> Bool

Eq a => CartesianClosedCategory (FinSet a) (Function a) (Set a) (FinSet (TwoProduct a)) (Function (TwoProduct a)) (Set (TwoProduct a)) (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a))

Defined in Math.Categories.FinSet

Methods

internalHom :: TwoBase (FinSet a) (Function a) (Set a) -> Tripod (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a))

type Rep (Exponential t)

Defined in Math.CartesianClosedCategory

type Rep (Exponential t) = D1 ('MetaData "Exponential" "Math.CartesianClosedCategory" "FiniteCategories-0.6.0.0-inplace" 'False) (C1 ('MetaCons "Exprojection" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)) :+: C1 ('MetaCons "ExponentialElement" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map t t))))

unexproject :: Exponential t -> t

Remove the constructor Exprojection from an original object t, throws an error if an ExponentialElement is given.

type Cartesian t = TwoProduct (Exponential t)

For a category to be cartesian closed, we need to construct 2-products of exponential objects with exprojected objects.

Exponential object

Candidate exponential object

isCandidateExponentialObject :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Tripod c m o -> Bool

Return wether a Tripod is a candidate exponential object or not. A Tripod is a candidate exponential object if its twoCone is a limit. Tests if the 2-cone is a 2-product by computing the limits in the universe category with the function limits : it is slow.

type CandidateExponentialObject c m o = Tripod c m o

A CandidateExponentialObject is a Tripod such that its twoCone is a limit.

Candidate exponential object morphism

data CandidateExponentialObjectMorphism c m o

A CandidateExponentialObjectMorphism is a morphism between two CandidateExponentialObjects. It is private, use smart constructors candidateExponentialObjectMorphism and unsafeCandidateExponentialObjectMorphism to instantiate.

Instances

(PrettyPrint o, PrettyPrint c, PrettyPrint m, Eq o, Eq m) => PrettyPrint (CandidateExponentialObjectMorphism c m o)

Defined in Math.CartesianClosedCategory

Methods

pprint :: Int -> CandidateExponentialObjectMorphism c m o -> String

pprintWithIndentations :: Int -> Int -> String -> CandidateExponentialObjectMorphism c m o -> String

pprintIndent :: Int -> CandidateExponentialObjectMorphism c m o -> String

(Simplifiable o, Simplifiable c, Simplifiable m) => Simplifiable (CandidateExponentialObjectMorphism c m o)

Defined in Math.CartesianClosedCategory

Methods

simplify :: CandidateExponentialObjectMorphism c m o -> CandidateExponentialObjectMorphism c m o

Generic (CandidateExponentialObjectMorphism c m o)

Defined in Math.CartesianClosedCategory

Associated Types

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

Methods

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

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

(Show o, Show c, Show m) => Show (CandidateExponentialObjectMorphism c m o)

Defined in Math.CartesianClosedCategory

Methods

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

show :: CandidateExponentialObjectMorphism c m o -> String

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

(Eq o, Eq c, Eq m) => Eq (CandidateExponentialObjectMorphism c m o)

Defined in Math.CartesianClosedCategory

Methods

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

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

Morphism m o => Morphism (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o)

Defined in Math.CartesianClosedCategory

Methods

(@) :: CandidateExponentialObjectMorphism c m o -> CandidateExponentialObjectMorphism c m o -> CandidateExponentialObjectMorphism c m o

(@?) :: CandidateExponentialObjectMorphism c m o -> CandidateExponentialObjectMorphism c m o -> Maybe (CandidateExponentialObjectMorphism c m o)

source :: CandidateExponentialObjectMorphism c m o -> CandidateExponentialObject c m o

target :: CandidateExponentialObjectMorphism c m o -> CandidateExponentialObject c m o

(Category c m o, Morphism m o, Eq c, Eq m, Eq o) => Category (CandidateExponentialObjectCategory c m o) (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o)

Defined in Math.CartesianClosedCategory

Methods

identity :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObject c m o -> CandidateExponentialObjectMorphism c m o

ar :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> Set (CandidateExponentialObjectMorphism c m o)

genAr :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> Set (CandidateExponentialObjectMorphism c m o)

decompose :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObjectMorphism c m o -> [CandidateExponentialObjectMorphism c m o]

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (CandidateExponentialObjectCategory c m o) (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o)

Defined in Math.CartesianClosedCategory

Methods

ob :: CandidateExponentialObjectCategory c m o -> Set (CandidateExponentialObject c m o)

type Rep (CandidateExponentialObjectMorphism c m o)

Defined in Math.CartesianClosedCategory

type Rep (CandidateExponentialObjectMorphism c m o) = D1 ('MetaData "CandidateExponentialObjectMorphism" "Math.CartesianClosedCategory" "FiniteCategories-0.6.0.0-inplace" 'False) (C1 ('MetaCons "CandidateExponentialObjectMorphism" 'PrefixI 'True) (S1 ('MetaSel ('Just "sourceCandidateExponentialObject") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CandidateExponentialObject c m o)) :*: (S1 ('MetaSel ('Just "targetCandidateExponentialObject") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (CandidateExponentialObject c m o)) :*: S1 ('MetaSel ('Just "transpose") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 m))))

Getters

transpose :: CandidateExponentialObjectMorphism c m o -> m

Smart constructors

candidateExponentialObjectMorphism :: (Morphism m o, Eq m, Eq o) => CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> m -> Maybe (CandidateExponentialObjectMorphism c m o)

Smart constructor for CandidateExponentialObjectMorphism. Checks wether the transpose has valid domain and valid codomain.

unsafeCandidateExponentialObjectMorphism :: CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> m -> CandidateExponentialObjectMorphism c m o

Unsafe version of candidateExponentialObjectMorphism, use with caution as it does not check wether the transpose has valid domain and valid codomain.

Candidate exponential object category,

data CandidateExponentialObjectCategory c m o

Constructors

CandidateExponentialObjectCategory (TwoBase c m o)

Instances

(PrettyPrint c, PrettyPrint o, PrettyPrint m, Eq o, Eq m) => PrettyPrint (CandidateExponentialObjectCategory c m o)

Defined in Math.CartesianClosedCategory

Methods

pprint :: Int -> CandidateExponentialObjectCategory c m o -> String

pprintWithIndentations :: Int -> Int -> String -> CandidateExponentialObjectCategory c m o -> String

pprintIndent :: Int -> CandidateExponentialObjectCategory c m o -> String

(Simplifiable c, Simplifiable o, Simplifiable m) => Simplifiable (CandidateExponentialObjectCategory c m o)

Defined in Math.CartesianClosedCategory

Methods

simplify :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObjectCategory c m o

Generic (CandidateExponentialObjectCategory c m o)

Defined in Math.CartesianClosedCategory

Associated Types

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

Methods

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

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

(Show c, Show o, Show m) => Show (CandidateExponentialObjectCategory c m o)

Defined in Math.CartesianClosedCategory

Methods

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

show :: CandidateExponentialObjectCategory c m o -> String

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

(Eq c, Eq m, Eq o) => Eq (CandidateExponentialObjectCategory c m o)

Defined in Math.CartesianClosedCategory

Methods

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

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

(Category c m o, Morphism m o, Eq c, Eq m, Eq o) => Category (CandidateExponentialObjectCategory c m o) (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o)

Defined in Math.CartesianClosedCategory

Methods

identity :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObject c m o -> CandidateExponentialObjectMorphism c m o

ar :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> Set (CandidateExponentialObjectMorphism c m o)

genAr :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> Set (CandidateExponentialObjectMorphism c m o)

decompose :: CandidateExponentialObjectCategory c m o -> CandidateExponentialObjectMorphism c m o -> [CandidateExponentialObjectMorphism c m o]

(FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (CandidateExponentialObjectCategory c m o) (CandidateExponentialObjectMorphism c m o) (CandidateExponentialObject c m o)

Defined in Math.CartesianClosedCategory

Methods

ob :: CandidateExponentialObjectCategory c m o -> Set (CandidateExponentialObject c m o)

type Rep (CandidateExponentialObjectCategory c m o)

Defined in Math.CartesianClosedCategory

type Rep (CandidateExponentialObjectCategory c m o) = D1 ('MetaData "CandidateExponentialObjectCategory" "Math.CartesianClosedCategory" "FiniteCategories-0.6.0.0-inplace" 'False) (C1 ('MetaCons "CandidateExponentialObjectCategory" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TwoBase c m o))))

Exponential object function

exponentialObjects :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => TwoBase c m o -> Set (CandidateExponentialObject c m o)

Return the exponential objects of a given 2-base.