Data.Functor.Invariant.Day

The Day convolution of two invariant functors is an invariant functor.

http://ncatlab.org/nlab/show/Day+convolution

Documentation

data Day f g a

The Day convolution of two invariant functors.

Constructors

forall b c. Day (f b) (g c) (b -> c -> a) (a -> (b, c))

Instances

Invariant (Day f g)

Defined in Data.Functor.Invariant.Day

Methods

invmap :: (a -> b) -> (b -> a) -> Day f g a -> Day f g b

day :: f a -> g b -> Day f g (a, b)

Construct the Day convolution

assoc :: Day f (Day g h) a -> Day (Day f g) h a

Day convolution provides a monoidal product. The associativity of this monoid is witnessed by assoc and disassoc.

assoc . disassoc = id
disassoc . assoc = id
invmap f g . assoc = assoc . invmap f g

disassoc :: Day (Day f g) h a -> Day f (Day g h) a

Day convolution provides a monoidal product. The associativity of this monoid is witnessed by assoc and disassoc.

assoc . disassoc = id
disassoc . assoc = id
invmap f g . disassoc = disassoc . invmap f g

swapped :: Day f g a -> Day g f a

The monoid for Day convolution on the cartesian monoidal structure is symmetric.

invmap f g . swapped = swapped . invmap f g

intro1 :: f a -> Day Identity f a

Identity is the unit of Day convolution

intro1 . elim1 = id
elim1 . intro1 = id

intro2 :: f a -> Day f Identity a

Identity is the unit of Day convolution

intro2 . elim2 = id
elim2 . intro2 = id

elim1 :: Invariant f => Day Identity f a -> f a

Identity is the unit of Day convolution

intro1 . elim1 = id
elim1 . intro1 = id

elim2 :: Invariant f => Day f Identity a -> f a

Identity is the unit of Day convolution

intro2 . elim2 = id
elim2 . intro2 = id

trans1 :: (forall x. f x -> g x) -> Day f h a -> Day g h a

Apply a natural transformation to the left-hand side of a Day convolution.

This respects the naturality of the natural transformation you supplied:

invmap f g . trans1 fg = trans1 fg . invmap f g

trans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a

Apply a natural transformation to the right-hand side of a Day convolution.

This respects the naturality of the natural transformation you supplied:

invmap f g . trans2 fg = trans2 fg . invmap f g

toContravariant :: Day f g a -> Day f g a

Drop the covariant part of the Day convolution.

toCovariant :: Day f g a -> Day f g a

Drop the contravariant part of the Day convolution.