Copyright | Guillaume Sabbagh 2022 |
---|---|
License | GPL-3 |
Maintainer | guillaumesabbagh@protonmail.com |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- type TwoBase c m o = Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o
- data Tripod c m o
- twoCone :: Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o
- evalMap :: Tripod c m o -> m
- internalDomain :: Morphism m o => Tripod c m o -> o
- internalCodomain :: Morphism m o => Tripod c m o -> o
- powerObject :: Morphism m o => Tripod c m o -> o
- universeCategoryTripod :: (Category c m o, Morphism m o, Eq c, Eq m, Eq o) => Tripod c m o -> c
- tripod :: (Morphism m o, Eq o) => Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o -> m -> Maybe (Tripod c m o)
- unsafeTripod :: Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o -> m -> Tripod c m o
- 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
- internalHom :: CompleteCategory c m o cLim mLim oLim DiscreteTwo DiscreteTwoAr DiscreteTwoOb => TwoBase c m o -> Tripod cLimExp mLimExp oLimExp
- type TwoProduct t = Limit DiscreteTwoOb t
- data Exponential t
- = Exprojection t
- | ExponentialElement (Map t t)
- unexproject :: Exponential t -> t
- type Cartesian t = TwoProduct (Exponential t)
- isCandidateExponentialObject :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => Tripod c m o -> Bool
- type CandidateExponentialObject c m o = Tripod c m o
- data CandidateExponentialObjectMorphism c m o
- transpose :: CandidateExponentialObjectMorphism c m o -> m
- candidateExponentialObjectMorphism :: (Morphism m o, Eq m, Eq o) => CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> m -> Maybe (CandidateExponentialObjectMorphism c m o)
- unsafeCandidateExponentialObjectMorphism :: CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> m -> CandidateExponentialObjectMorphism c m o
- data CandidateExponentialObjectCategory c m o = CandidateExponentialObjectCategory (TwoBase c m o)
- exponentialObjects :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => TwoBase c m o -> Set (CandidateExponentialObject c m o)
2-base
type TwoBase c m o = Diagram DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o Source #
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
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
Getters
twoCone :: Tripod c m o -> Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o Source #
evalMap :: Tripod c m o -> m Source #
The evaluation map should go from the apex of the 2-cone to the internal codomain
internalCodomain :: Morphism m o => Tripod c m o -> o Source #
Return the internal codomain of a Tripod
.
universeCategoryTripod :: (Category c m o, Morphism m o, Eq c, Eq m, Eq o) => Tripod c m o -> c Source #
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) Source #
unsafeTripod :: Cone DiscreteTwo DiscreteTwoAr DiscreteTwoOb c m o -> m -> Tripod c m o Source #
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 Source #
internalHom :: CompleteCategory c m o cLim mLim oLim DiscreteTwo DiscreteTwoAr DiscreteTwoOb => TwoBase c m o -> Tripod cLimExp mLimExp oLimExp Source #
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)) Source # | |
type TwoProduct t = Limit DiscreteTwoOb t Source #
For a category to be cartesian closed, we need to construct 2-products.
data Exponential t Source #
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 Exprojection
s.
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]).
Exprojection t | A |
ExponentialElement (Map t t) | An |
Instances
(PrettyPrint t, Eq t) => PrettyPrint (Exponential t) Source # | |
Defined in Math.CartesianClosedCategory pprint :: Int -> Exponential t -> String Source # pprintWithIndentations :: Int -> Int -> String -> Exponential t -> String Source # pprintIndent :: Int -> Exponential t -> String Source # | |
(Simplifiable t, Eq t) => Simplifiable (Exponential t) Source # | |
Defined in Math.CartesianClosedCategory simplify :: Exponential t -> Exponential t # | |
Generic (Exponential t) Source # | |
Defined in Math.CartesianClosedCategory type Rep (Exponential t) :: Type -> Type from :: Exponential t -> Rep (Exponential t) x to :: Rep (Exponential t) x -> Exponential t | |
Show t => Show (Exponential t) Source # | |
Defined in Math.CartesianClosedCategory showsPrec :: Int -> Exponential t -> ShowS show :: Exponential t -> String showList :: [Exponential t] -> ShowS | |
Eq t => Eq (Exponential t) Source # | |
Defined in Math.CartesianClosedCategory (==) :: 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)) Source # | |
type Rep (Exponential t) Source # | |
Defined in Math.CartesianClosedCategory type Rep (Exponential t) = D1 ('MetaData "Exponential" "Math.CartesianClosedCategory" "FiniteCategories-0.6.1.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 Source #
Remove the constructor Exprojection
from an original object t, throws an error if an ExponentialElement
is given.
type Cartesian t = TwoProduct (Exponential t) Source #
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 Source #
type CandidateExponentialObject c m o = Tripod c m o Source #
A CandidateExponentialObject
is a Tripod
such that its twoCone
is a limit.
Candidate exponential object morphism
data CandidateExponentialObjectMorphism c m o Source #
A CandidateExponentialObjectMorphism
is a morphism between two CandidateExponentialObject
s. It is private, use smart constructors candidateExponentialObjectMorphism
and unsafeCandidateExponentialObjectMorphism
to instantiate.
Instances
Getters
transpose :: CandidateExponentialObjectMorphism c m o -> m Source #
Smart constructors
candidateExponentialObjectMorphism :: (Morphism m o, Eq m, Eq o) => CandidateExponentialObject c m o -> CandidateExponentialObject c m o -> m -> Maybe (CandidateExponentialObjectMorphism c m o) Source #
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 Source #
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 Source #
Instances
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) Source #
Return the exponential objects of a given 2-base.