| Copyright | Guillaume Sabbagh 2023 |
|---|---|
| License | GPL-3 |
| Maintainer | guillaumesabbagh@protonmail.com |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Math.Functors.SetValued
Description
Kan extensions for set-valued functors. Inspired by DBC of M. Fleming, R. Gunther, R. Rosebrugh.
Synopsis
- type LimitObject o1 m2 a = Map (CommaObject One o1 m2) a
- rightKanSetValued :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) => Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> (Diagram c2 m2 o2 (FinSet (LimitObject o1 m2 a)) (Function (LimitObject o1 m2 a)) (Set (LimitObject o1 m2 a)), NaturalTransformation c1 m1 o1 (FinSet (LimitObject o1 m2 a)) (Function (LimitObject o1 m2 a)) (Set (LimitObject o1 m2 a)))
- formatLimitObject :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => LimitObject o1 m2 a -> String
- formatSetOfLimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Set (LimitObject o1 m2 a) -> String
- formatFunctionOfLimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Function (LimitObject o1 m2 a) -> String
- type ColimitObject o1 m2 a = Set (CommaObject o1 One m2, a)
- leftKanSetValued :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) => Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> (Diagram c2 m2 o2 (FinSet (ColimitObject o1 m2 a)) (Function (ColimitObject o1 m2 a)) (Set (ColimitObject o1 m2 a)), NaturalTransformation c1 m1 o1 (FinSet (ColimitObject o1 m2 a)) (Function (ColimitObject o1 m2 a)) (Set (ColimitObject o1 m2 a)))
- formatColimitObject :: PrettyPrint a => ColimitObject o1 m2 a -> String
- formatSetOfColimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Set (ColimitObject o1 m2 a) -> String
- formatFunctionOfColimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Function (ColimitObject o1 m2 a) -> String
Right Kan extension
type LimitObject o1 m2 a = Map (CommaObject One o1 m2) a Source #
A LimitObject is a map from a comma object to an element a, the maps should be seen as elements of the cartesian products indexed by comma objects.
rightKanSetValued :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) => Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> (Diagram c2 m2 o2 (FinSet (LimitObject o1 m2 a)) (Function (LimitObject o1 m2 a)) (Set (LimitObject o1 m2 a)), NaturalTransformation c1 m1 o1 (FinSet (LimitObject o1 m2 a)) (Function (LimitObject o1 m2 a)) (Set (LimitObject o1 m2 a))) Source #
The right Kan extension of X along F where X is a a set-valued functor.
We transform the X functor so that its target becomes (FinSet (Map (CommaObject One o1 m2) a)), each object A of c1 is mapped to {Delta : {One,id,A} -> e | e <- X(A)}.
Formatting
formatLimitObject :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => LimitObject o1 m2 a -> String Source #
Format a LimitObject to be readable.
formatSetOfLimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Set (LimitObject o1 m2 a) -> String Source #
Format a set of LimitObjects to be readable.
formatFunctionOfLimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Function (LimitObject o1 m2 a) -> String Source #
Format a Function of LimitObjects to be readable.
Left Kan extension
type ColimitObject o1 m2 a = Set (CommaObject o1 One m2, a) Source #
A ColimitObject is a set of couples (comma objects, elements a), the couples should be seen as elements of a disjoint union, the set of couples as equivalence classes of elements of a disjoint union.
leftKanSetValued :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, Eq a) => Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (FinSet a) (Function a) (Set a) -> (Diagram c2 m2 o2 (FinSet (ColimitObject o1 m2 a)) (Function (ColimitObject o1 m2 a)) (Set (ColimitObject o1 m2 a)), NaturalTransformation c1 m1 o1 (FinSet (ColimitObject o1 m2 a)) (Function (ColimitObject o1 m2 a)) (Set (ColimitObject o1 m2 a))) Source #
The left Kan extension of X along F where X is a a set-valued functor.
We transform the X functor so that its target becomes (FinSet (Set ((CommaObject One o1 m2), a))), each object A of c1 is mapped to {(One,id,A},e) | e <- X(A)}.
Formatting
formatColimitObject :: PrettyPrint a => ColimitObject o1 m2 a -> String Source #
Format a ColimitObject to be readable.
formatSetOfColimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Set (ColimitObject o1 m2 a) -> String Source #
Format a set of ColimitObjects to be readable.
formatFunctionOfColimitObjects :: (Eq o1, Eq m2, Eq a, PrettyPrint a) => Function (ColimitObject o1 m2 a) -> String Source #
Format a Function of ColimitObjects to be readable.