{-# LANGUAGE TypeOperators, TypeFamilies, PatternSynonyms, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, LiberalTypeSynonyms, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.NaturalTransformation
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.NaturalTransformation (

  -- * Natural transformations
    (:~>)
  , Component
  , (!)
  , o
  , natId
  , srcF
  , tgtF

  -- * Functor category
  , Nat(..)
  , Endo
  , Presheaves
  , Profunctors

  -- * Functor isomorphisms
  , compAssoc
  , compAssocInv
  , idPrecomp
  , idPrecompInv
  , idPostcomp
  , idPostcompInv
  , constPrecompIn
  , constPrecompOut
  , constPostcompIn
  , constPostcompOut

  -- * Related functors
  , FunctorCompose(..)
  , EndoFunctorCompose
  , Precompose, pattern Precompose
  , Postcompose, pattern Postcompose
  , Wrap(..)
  , Apply(..)
  , Tuple(..)

) where

import Data.Category
import Data.Category.Functor
import Data.Category.Product

infixl 9 !

-- | @f :~> g@ is a natural transformation from functor f to functor g.
type f :~> g = forall c d. (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g

-- | Natural transformations are built up of components,
-- one for each object @z@ in the domain category of @f@ and @g@.
data Nat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
  Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g)
    => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g


-- | A component for an object @z@ is an arrow from @F z@ to @G z@.
type Component f g z = Cod f (f :% z) (g :% z)

-- | 'n ! a' returns the component for the object @a@ of a natural transformation @n@.
--   This can be generalized to any arrow (instead of just identity arrows).
(!) :: (Category c, Category d) => Nat c d f g -> c a b -> d (f :% a) (g :% b)
Nat f
f g
_ forall z. Obj c z -> Component f g z
n ! :: Nat c d f g -> c a b -> d (f :% a) (g :% b)
! c a b
h = Obj c b -> Component f g b
forall z. Obj c z -> Component f g z
n (c a b -> Obj c b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt c a b
h) d (f :% b) (g :% b) -> d (f :% a) (f :% b) -> d (f :% a) (g :% b)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. f
f f -> Dom f a b -> Cod f (f :% a) (f :% b)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% c a b
Dom f a b
h -- or g % h . n (src h), or n h when h is an identity arrow


-- | Horizontal composition of natural transformations.
o :: (Category c, Category d, Category e) => Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
njk :: Nat d e j k
njk@(Nat j
j k
k forall z. Obj d z -> Component j k z
_) o :: Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` nfg :: Nat c d f g
nfg@(Nat f
f g
g forall z. Obj c z -> Component f g z
_) = (j :.: f)
-> (k :.: g)
-> (forall z. Obj c z -> Component (j :.: f) (k :.: g) z)
-> Nat c e (j :.: f) (k :.: g)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (j
j j -> f -> j :.: f
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) (k
k k -> g -> k :.: g
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g) ((Nat d e j k
njk Nat d e j k
-> d (f :% z) (g :% z) -> e (j :% (f :% z)) (k :% (g :% z))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!) (d (f :% z) (g :% z) -> e (j :% (f :% z)) (k :% (g :% z)))
-> (c z z -> d (f :% z) (g :% z))
-> c z z
-> e (j :% (f :% z)) (k :% (g :% z))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Nat c d f g
nfg Nat c d f g -> c z z -> d (f :% z) (g :% z)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!))
-- Nat j k njk `o` Nat f g nfg = Nat (j :.: f) (k :.: g) (\x -> njk (g % x) . j % nfg x) -- or k % nfg x . njk (f % x)

-- | The identity natural transformation of a functor.
natId :: Functor f => f -> Nat (Dom f) (Cod f) f f
natId :: f -> Nat (Dom f) (Cod f) f f
natId f
f = f
-> f
-> (forall z. Obj (Dom f) z -> Component f f z)
-> Nat (Dom f) (Cod f) f f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f f
f (\Obj (Dom f) z
i -> f
f f -> Obj (Dom f) z -> Component f f z
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (Dom f) z
i)

pattern NatId :: Functor f => f -> Nat (Dom f) (Cod f) f f
pattern $bNatId :: f -> Nat (Dom f) (Cod f) f f
$mNatId :: forall r f.
Functor f =>
Nat (Dom f) (Cod f) f f -> (f -> r) -> (Void# -> r) -> r
NatId f <- Nat f _ _ where 
  NatId f
f = f
-> f
-> (forall z. Obj (Dom f) z -> Component f f z)
-> Nat (Dom f) (Cod f) f f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f f
f (\Obj (Dom f) z
i -> f
f f -> Obj (Dom f) z -> Component f f z
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (Dom f) z
i)

srcF :: Nat c d f g -> f
srcF :: Nat c d f g -> f
srcF (Nat f
f g
_ forall z. Obj c z -> Component f g z
_) = f
f

tgtF :: Nat c d f g -> g
tgtF :: Nat c d f g -> g
tgtF (Nat f
_ g
g forall z. Obj c z -> Component f g z
_) = g
g

-- | Functor category D^C.
-- Objects of D^C are functors from C to D.
-- Arrows of D^C are natural transformations.
instance Category d => Category (Nat c d) where

  src :: Nat c d a b -> Obj (Nat c d) a
src (Nat a
f b
_ forall z. Obj c z -> Component a b z
_)           = a -> Nat (Dom a) (Cod a) a a
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId a
f
  tgt :: Nat c d a b -> Obj (Nat c d) b
tgt (Nat a
_ b
g forall z. Obj c z -> Component a b z
_)           = b -> Nat (Dom b) (Cod b) b b
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId b
g

  Nat b
_ c
h forall z. Obj c z -> Component b c z
ngh . :: Nat c d b c -> Nat c d a b -> Nat c d a c
. Nat a
f b
_ forall z. Obj c z -> Component a b z
nfg = a -> c -> (forall z. Obj c z -> Component a c z) -> Nat c d a c
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat a
f c
h (\Obj c z
i -> Obj c z -> Component b c z
forall z. Obj c z -> Component b c z
ngh Obj c z
i d (b :% z) (c :% z) -> d (a :% z) (b :% z) -> d (a :% z) (c :% z)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj c z -> Component a b z
forall z. Obj c z -> Component a b z
nfg Obj c z
i)


compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h)
          => f -> g -> h -> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
compAssoc :: f
-> g
-> h
-> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
compAssoc f
f g
g h
h = ((f :.: g) :.: h)
-> (f :.: (g :.: h))
-> (forall z.
    Obj (Dom h) z -> Component ((f :.: g) :.: h) (f :.: (g :.: h)) z)
-> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat ((f
f f -> g -> f :.: g
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g) (f :.: g) -> h -> (f :.: g) :.: h
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: h
h) (f
f f -> (g :.: h) -> f :.: (g :.: h)
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: (g
g g -> h -> g :.: h
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: h
h)) (\Obj (Dom h) z
i -> f
f f
-> Dom f (g :% (h :% z)) (g :% (h :% z))
-> Cod f (f :% (g :% (h :% z))) (f :% (g :% (h :% z)))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% g
g g
-> Dom g (h :% z) (h :% z) -> Cod g (g :% (h :% z)) (g :% (h :% z))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% h
h h -> Obj (Dom h) z -> Cod h (h :% z) (h :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (Dom h) z
i)

compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h)
             => f -> g -> h -> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
compAssocInv :: f
-> g
-> h
-> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
compAssocInv f
f g
g h
h = (f :.: (g :.: h))
-> ((f :.: g) :.: h)
-> (forall z.
    Obj (Dom h) z -> Component (f :.: (g :.: h)) ((f :.: g) :.: h) z)
-> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (f
f f -> (g :.: h) -> f :.: (g :.: h)
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: (g
g g -> h -> g :.: h
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: h
h)) ((f
f f -> g -> f :.: g
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g) (f :.: g) -> h -> (f :.: g) :.: h
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: h
h) (\Obj (Dom h) z
i -> f
f f
-> Dom f (g :% (h :% z)) (g :% (h :% z))
-> Cod f (f :% (g :% (h :% z))) (f :% (g :% (h :% z)))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% g
g g
-> Dom g (h :% z) (h :% z) -> Cod g (g :% (h :% z)) (g :% (h :% z))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% h
h h -> Obj (Dom h) z -> Cod h (h :% z) (h :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj (Dom h) z
i)

idPrecomp :: Functor f => f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp :: f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp f
f = (f :.: Id (Dom f))
-> f
-> (forall z. Obj (Dom f) z -> Component (f :.: Id (Dom f)) f z)
-> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (f
f f -> Id (Dom f) -> f :.: Id (Dom f)
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: Id (Dom f)
forall (k :: * -> * -> *). Id k
Id) f
f (f
f f -> Dom f z z -> Cod f (f :% z) (f :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
%)

idPrecompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv :: f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv f
f = f
-> (f :.: Id (Dom f))
-> (forall z. Obj (Dom f) z -> Component f (f :.: Id (Dom f)) z)
-> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (f
f f -> Id (Dom f) -> f :.: Id (Dom f)
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: Id (Dom f)
forall (k :: * -> * -> *). Id k
Id) (f
f f -> Dom f z z -> Cod f (f :% z) (f :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
%)

idPostcomp :: Functor f => f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
idPostcomp :: f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
idPostcomp f
f = (Id (Cod f) :.: f)
-> f
-> (forall z. Obj (Dom f) z -> Component (Id (Cod f) :.: f) f z)
-> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Id (Cod f)
forall (k :: * -> * -> *). Id k
Id Id (Cod f) -> f -> Id (Cod f) :.: f
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) f
f (f
f f -> Dom f z z -> Cod f (f :% z) (f :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
%)

idPostcompInv :: Functor f => f -> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f)
idPostcompInv :: f -> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f)
idPostcompInv f
f = f
-> (Id (Cod f) :.: f)
-> (forall z. Obj (Dom f) z -> Component f (Id (Cod f) :.: f) z)
-> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (Id (Cod f)
forall (k :: * -> * -> *). Id k
Id Id (Cod f) -> f -> Id (Cod f) :.: f
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) (f
f f -> Dom f z z -> Cod f (f :% z) (f :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
%)


constPrecompIn :: Nat j d (f :.: Const j c x) g -> Nat j d (Const j d (f :% x)) g
constPrecompIn :: Nat j d (f :.: Const j c x) g -> Nat j d (Const j d (f :% x)) g
constPrecompIn (Nat (f
f :.: Const Obj c x
x) g
g forall z. Obj j z -> Component (f :.: Const j c x) g z
n) = Const j d (f :% x)
-> g
-> (forall z. Obj j z -> Component (Const j d (f :% x)) g z)
-> Nat j d (Const j d (f :% x)) g
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj d (f :% x) -> Const j d (f :% x)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f f -> Dom f x x -> Cod f (f :% x) (f :% x)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c x
Dom f x x
x)) g
g forall z. Obj j z -> Component (Const j d (f :% x)) g z
forall z. Obj j z -> Component (f :.: Const j c x) g z
n

constPrecompOut :: Nat j d f (g :.: Const j c x) -> Nat j d f (Const j d (g :% x))
constPrecompOut :: Nat j d f (g :.: Const j c x) -> Nat j d f (Const j d (g :% x))
constPrecompOut (Nat f
f (g
g :.: Const Obj c x
x) forall z. Obj j z -> Component f (g :.: Const j c x) z
n) = f
-> Const j d (g :% x)
-> (forall z. Obj j z -> Component f (Const j d (g :% x)) z)
-> Nat j d f (Const j d (g :% x))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (Obj d (g :% x) -> Const j d (g :% x)
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (g
g g -> Dom g x x -> Cod g (g :% x) (g :% x)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c x
Dom g x x
x)) forall z. Obj j z -> Component f (Const j d (g :% x)) z
forall z. Obj j z -> Component f (g :.: Const j c x) z
n

constPostcompIn :: Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g
constPostcompIn :: Nat j d (Const k d x :.: f) g -> Nat j d (Const j d x) g
constPostcompIn (Nat (Const Obj d x
x :.: f
_) g
g forall z. Obj j z -> Component (Const k d x :.: f) g z
n) = Const j d x
-> g
-> (forall z. Obj j z -> Component (Const j d x) g z)
-> Nat j d (Const j d x) g
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj d x -> Const j d x
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj d x
x) g
g forall z. Obj j z -> Component (Const j d x) g z
forall z. Obj j z -> Component (Const k d x :.: f) g z
n

constPostcompOut :: Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x)
constPostcompOut :: Nat j d f (Const k d x :.: g) -> Nat j d f (Const j d x)
constPostcompOut (Nat f
f (Const Obj d x
x :.: g
_) forall z. Obj j z -> Component f (Const k d x :.: g) z
n) = f
-> Const j d x
-> (forall z. Obj j z -> Component f (Const j d x) z)
-> Nat j d f (Const j d x)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (Obj d x -> Const j d x
forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj d x
x) forall z. Obj j z -> Component f (Const j d x) z
forall z. Obj j z -> Component f (Const k d x :.: g) z
n


data FunctorCompose (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) = FunctorCompose

-- | Composition of functors is a functor.
instance (Category c, Category d, Category e) => Functor (FunctorCompose c d e) where
  type Dom (FunctorCompose c d e) = Nat d e :**: Nat c d
  type Cod (FunctorCompose c d e) = Nat c e
  type FunctorCompose c d e :% (f, g) = f :.: g

  FunctorCompose c d e
FunctorCompose % :: FunctorCompose c d e
-> Dom (FunctorCompose c d e) a b
-> Cod
     (FunctorCompose c d e)
     (FunctorCompose c d e :% a)
     (FunctorCompose c d e :% b)
% (n1 :**: n2) = Nat d e a1 b1
n1 Nat d e a1 b1 -> Nat c d a2 b2 -> Nat c e (a1 :.: a2) (b1 :.: b2)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Nat c d a2 b2
n2


-- | The category of endofunctors.
type Endo k = Nat k k
-- | Composition of endofunctors is a functor.
type EndoFunctorCompose k = FunctorCompose k k k

type Presheaves k = Nat (Op k) (->)

type Profunctors c d = Nat (Op d :**: c) (->)

-- | @Precompose f e@ is the functor such that @Precompose f e :% g = g :.: f@,
--   for functors @g@ that compose with @f@ and with codomain @e@.
type Precompose f e = FunctorCompose (Dom f) (Cod f) e :.: Tuple2 (Nat (Cod f) e) (Nat (Dom f) (Cod f)) f
pattern Precompose :: (Category e, Functor f) => f -> Precompose f e
pattern $bPrecompose :: f -> Precompose f e
$mPrecompose :: forall r (e :: * -> * -> *) f.
(Category e, Functor f) =>
Precompose f e -> (f -> r) -> (Void# -> r) -> r
Precompose f = FunctorCompose :.: Tuple2 (NatId f)

-- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@,
--   for functors @g@ that compose with @f@ and with domain @c@.
type Postcompose f c = FunctorCompose c (Dom f) (Cod f) :.: Tuple1 (Nat (Dom f) (Cod f)) (Nat c (Dom f)) f
pattern Postcompose :: (Category e, Functor f) => f -> Postcompose f e
pattern $bPostcompose :: f -> Postcompose f e
$mPostcompose :: forall r (e :: * -> * -> *) f.
(Category e, Functor f) =>
Postcompose f e -> (f -> r) -> (Void# -> r) -> r
Postcompose f = FunctorCompose :.: Tuple1 (NatId f)


data Wrap f h = Wrap f h

-- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@,
--   for functors @g@ that compose with @f@ and @h@.
instance (Functor f, Functor h) => Functor (Wrap f h) where
  type Dom (Wrap f h) = Nat (Cod h) (Dom f)
  type Cod (Wrap f h) = Nat (Dom h) (Cod f)
  type Wrap f h :% g = f :.: g :.: h

  Wrap f
f h
h % :: Wrap f h
-> Dom (Wrap f h) a b
-> Cod (Wrap f h) (Wrap f h :% a) (Wrap f h :% b)
% Dom (Wrap f h) a b
n = f -> Nat (Dom f) (Cod f) f f
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId f
f Nat (Dom f) (Cod f) f f
-> Nat (Cod h) (Dom f) a b
-> Nat (Cod h) (Cod f) (f :.: a) (f :.: b)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` Dom (Wrap f h) a b
Nat (Cod h) (Dom f) a b
n Nat (Cod h) (Cod f) (f :.: a) (f :.: b)
-> Nat (Dom h) (Cod h) h h
-> Nat (Dom h) (Cod f) ((f :.: a) :.: h) ((f :.: b) :.: h)
forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` h -> Nat (Dom h) (Cod h) h h
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId h
h


data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Apply
-- | 'Apply' is a bifunctor, @Apply :% (f, a)@ applies @f@ to @a@, i.e. @f :% a@.
instance (Category c1, Category c2) => Functor (Apply c1 c2) where
  type Dom (Apply c1 c2) = Nat c2 c1 :**: c2
  type Cod (Apply c1 c2) = c1
  type Apply c1 c2 :% (f, a) = f :% a
  Apply c1 c2
Apply % :: Apply c1 c2
-> Dom (Apply c1 c2) a b
-> Cod (Apply c1 c2) (Apply c1 c2 :% a) (Apply c1 c2 :% b)
% (l :**: r) = Nat c2 c1 a1 b1
l Nat c2 c1 a1 b1 -> c2 a2 b2 -> c1 (a1 :% a2) (b1 :% b2)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! c2 a2 b2
r

data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Tuple
-- | 'Tuple' converts an object @a@ to the functor 'Tuple1' @a@.
instance (Category c1, Category c2) => Functor (Tuple c1 c2) where
  type Dom (Tuple c1 c2) = c1
  type Cod (Tuple c1 c2) = Nat c2 (c1 :**: c2)
  type Tuple c1 c2 :% a = Tuple1 c1 c2 a
  Tuple c1 c2
Tuple % :: Tuple c1 c2
-> Dom (Tuple c1 c2) a b
-> Cod (Tuple c1 c2) (Tuple c1 c2 :% a) (Tuple c1 c2 :% b)
% Dom (Tuple c1 c2) a b
f = Tuple1 c1 c2 a
-> Tuple1 c1 c2 b
-> (forall z.
    Obj c2 z -> Component (Tuple1 c1 c2 a) (Tuple1 c1 c2 b) z)
-> Nat c2 (c1 :**: c2) (Tuple1 c1 c2 a) (Tuple1 c1 c2 b)
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj c1 a -> Tuple1 c1 c2 a
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c1 a -> Tuple1 c1 c2 a
Tuple1 (c1 a b -> Obj c1 a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src c1 a b
Dom (Tuple c1 c2) a b
f)) (Obj c1 b -> Tuple1 c1 c2 b
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c1 a -> Tuple1 c1 c2 a
Tuple1 (c1 a b -> Obj c1 b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt c1 a b
Dom (Tuple c1 c2) a b
f)) (\Obj c2 z
z -> c1 a b
Dom (Tuple c1 c2) a b
f c1 a b -> Obj c2 z -> (:**:) c1 c2 (a, z) (b, z)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: Obj c2 z
z)