{-# 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
  , pattern 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
  , Curry1, pattern Curry1
  , Curry2, pattern Curry2
  , Wrap(..)
  , Apply(..)
  , Tuple(..)
  , Opp(..), Opposite, pattern Opposite
  , HomF, pattern HomF
  , Star, pattern Star
  , Costar, pattern Costar
  , (:*%:), pattern HomXF
  , (:%*:), pattern HomFX

) where

import Data.Kind (Type)

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 :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type 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 ! :: forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! c a b
h = forall z. Obj c z -> Component f g z
n (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt c a b
h) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% c 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 :: 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` nfg :: Nat c d f g
nfg@(Nat f
f g
g forall z. Obj c z -> Component f g z
_) = 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 forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) (k
k forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g) ((Nat d e j k
njk forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a 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
. (Nat c d f g
nfg 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 :: forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId 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 (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
%)

pattern NatId :: () => (Functor f, c ~ Dom f, d ~ Cod f) => f -> Nat c d f f
pattern $bNatId :: forall f (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, c ~ Dom f, d ~ Cod f) =>
f -> Nat c d f f
$mNatId :: forall {r} {f} {c :: * -> * -> *} {d :: * -> * -> *}.
Nat c d f f
-> ((Functor f, c ~ Dom f, d ~ Cod f) => f -> r)
-> ((# #) -> r)
-> r
NatId f <- Nat f _ _ where
  NatId 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 (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
%)
{-# COMPLETE NatId #-}

srcF :: Nat c d f g -> f
srcF :: forall (c :: * -> * -> *) (d :: * -> * -> *) f g. 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 :: forall (c :: * -> * -> *) (d :: * -> * -> *) f g. 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 :: forall a b. Nat c d a b -> Obj (Nat c d) a
src (Nat a
f b
_ forall z. Obj c z -> Component a b z
_)           = forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId a
f
  tgt :: forall a b. Nat c d a b -> Obj (Nat c d) b
tgt (Nat a
_ b
g forall z. Obj c z -> Component a b z
_)           = 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 . :: forall b c a. 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 = 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 -> forall z. Obj c z -> Component b c z
ngh Obj c z
i forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. 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 :: forall f g h.
(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
f g
g h
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 forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g) forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: h
h) (f
f forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: (g
g forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: h
h)) (\Obj (Dom h) z
i -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% h
h 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 :: forall f g h.
(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
f g
g h
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 forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: (g
g forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: h
h)) ((f
f forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g) forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: h
h) (\Obj (Dom h) z
i -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% h
h 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 :: forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp 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 forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: forall (k :: * -> * -> *). Id k
Id) f
f (f
f 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 :: forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv 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 forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: forall (k :: * -> * -> *). Id k
Id) (f
f 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 :: forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
idPostcomp 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 (forall (k :: * -> * -> *). Id k
Id forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) f
f (f
f 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 :: forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f)
idPostcompInv 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 (forall (k :: * -> * -> *). Id k
Id forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) (f
f 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 :: forall (j :: * -> * -> *) (d :: * -> * -> *) f (c :: * -> * -> *) x
       g.
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) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c x
x)) g
g 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 :: forall (j :: * -> * -> *) (d :: * -> * -> *) f g (c :: * -> * -> *)
       x.
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) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const (g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Obj c x
x)) 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 :: forall (j :: * -> * -> *) (d :: * -> * -> *) (k :: * -> * -> *) x f
       g.
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) = 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 (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 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 :: forall (j :: * -> * -> *) (d :: * -> * -> *) f (k :: * -> * -> *) x
       g.
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) = 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 (forall (c2 :: * -> * -> *) x (c1 :: * -> * -> *).
Obj c2 x -> Const c1 c2 x
Const Obj d x
x) forall z. Obj j z -> Component f (Const k d x :.: g) z
n


data FunctorCompose (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) (e :: Type -> Type -> Type) = 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 % :: forall a b.
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)
% (Nat d e a1 b1
n1 :**: Nat c d a2 b2
n2) = Nat d e a1 b1
n1 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 :: forall (e :: * -> * -> *) f.
(Category e, Functor f) =>
f -> Precompose f e
$mPrecompose :: forall {r} {e :: * -> * -> *} {f}.
(Category e, Functor f) =>
Precompose f e -> (f -> r) -> ((# #) -> 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 c, Functor f) => f -> Postcompose f c
pattern $bPostcompose :: forall (c :: * -> * -> *) f.
(Category c, Functor f) =>
f -> Postcompose f c
$mPostcompose :: forall {r} {c :: * -> * -> *} {f}.
(Category c, Functor f) =>
Postcompose f c -> (f -> r) -> ((# #) -> r) -> r
Postcompose f = FunctorCompose :.: Tuple1 (NatId f)


type Curry1 c1 c2 f = Postcompose f c2 :.: Tuple c1 c2
-- | Curry on the first "argument" of a functor from a product category.
pattern Curry1 :: (Functor f, Dom f ~ c1 :**: c2, Category c1, Category c2) => f -> Curry1 c1 c2 f
pattern $bCurry1 :: forall f (c1 :: * -> * -> *) (c2 :: * -> * -> *).
(Functor f, Dom f ~ (c1 :**: c2), Category c1, Category c2) =>
f -> Curry1 c1 c2 f
$mCurry1 :: forall {r} {f} {c1 :: * -> * -> *} {c2 :: * -> * -> *}.
(Functor f, Dom f ~ (c1 :**: c2), Category c1, Category c2) =>
Curry1 c1 c2 f -> (f -> r) -> ((# #) -> r) -> r
Curry1 f = Postcompose f :.: Tuple

type Curry2 c1 c2 f = Postcompose f c1 :.: Curry1 c2 c1 (Swap c2 c1)
-- | Curry on the second "argument" of a functor from a product category.
pattern Curry2 :: (Functor f, Dom f ~ c1 :**: c2, Category c1, Category c2) => f -> Curry2 c1 c2 f
pattern $bCurry2 :: forall f (c1 :: * -> * -> *) (c2 :: * -> * -> *).
(Functor f, Dom f ~ (c1 :**: c2), Category c1, Category c2) =>
f -> Curry2 c1 c2 f
$mCurry2 :: forall {r} {f} {c1 :: * -> * -> *} {c2 :: * -> * -> *}.
(Functor f, Dom f ~ (c1 :**: c2), Category c1, Category c2) =>
Curry2 c1 c2 f -> (f -> r) -> ((# #) -> r) -> r
Curry2 f = Postcompose f :.: Curry1 Swap


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 % :: forall a b.
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 = forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId f
f 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
n 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` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId h
h


data Apply (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = 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 % :: forall a b.
Apply c1 c2
-> Dom (Apply c1 c2) a b
-> Cod (Apply c1 c2) (Apply c1 c2 :% a) (Apply c1 c2 :% b)
% (Nat c2 c1 a1 b1
l :**: c2 a2 b2
r) = Nat c2 c1 a1 b1
l 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 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = 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 % :: forall a b.
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 = 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 (forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c1 a -> Tuple1 c1 c2 a
Tuple1 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (Tuple c1 c2) a b
f)) (forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c1 a -> Tuple1 c1 c2 a
Tuple1 (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (Tuple c1 c2) a b
f)) (Dom (Tuple c1 c2) a b
f forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**:)


data Opp (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) = Opp
-- | Turning a functor into its dual is contravariantly functorial.
instance (Category c1, Category c2) => Functor (Opp c1 c2) where
  type Dom (Opp c1 c2) = Op (Nat c1 c2) :**: Op c1
  type Cod (Opp c1 c2) = Op c2
  type Opp c1 c2 :% (f, a) = f :% a
  Opp c1 c2
Opp % :: forall a b.
Opp c1 c2
-> Dom (Opp c1 c2) a b
-> Cod (Opp c1 c2) (Opp c1 c2 :% a) (Opp c1 c2 :% b)
% (Op Nat c1 c2 b1 a1
n :**: Op c1 b2 a2
f) = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (Nat c1 c2 b1 a1
n forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! c1 b2 a2
f)

type Opposite f = Opp (Dom f) (Cod f) :.: Tuple1 (Op (Nat (Dom f) (Cod f))) (Op (Dom f)) f
-- | The dual of a functor
pattern Opposite :: Functor f => f -> Opposite f
pattern $bOpposite :: forall f. Functor f => f -> Opposite f
$mOpposite :: forall {r} {f}.
Functor f =>
Opposite f -> (f -> r) -> ((# #) -> r) -> r
Opposite f = Opp :.: Tuple1 (Op (NatId f))
{-# COMPLETE Opposite #-}


type HomF f g = Hom (Cod f) :.: (Opposite f :***: g)
pattern HomF :: (Functor f, Functor g, Cod f ~ Cod g) => f -> g -> HomF f g
pattern $bHomF :: forall f g.
(Functor f, Functor g, Cod f ~ Cod g) =>
f -> g -> HomF f g
$mHomF :: forall {r} {f} {g}.
(Functor f, Functor g, Cod f ~ Cod g) =>
HomF f g -> (f -> g -> r) -> ((# #) -> r) -> r
HomF f g = Hom :.: (Opposite f :***: g)
{-# COMPLETE HomF #-}

type Star f = HomF (Id (Cod f)) f
pattern Star :: Functor f => f -> Star f
pattern $bStar :: forall f. Functor f => f -> Star f
$mStar :: forall {r} {f}.
Functor f =>
Star f -> (f -> r) -> ((# #) -> r) -> r
Star f = HomF Id f
{-# COMPLETE Star #-}

type Costar f = HomF f (Id (Cod f))
pattern Costar :: Functor f => f -> Costar f
pattern $bCostar :: forall f. Functor f => f -> Costar f
$mCostar :: forall {r} {f}.
Functor f =>
Costar f -> (f -> r) -> ((# #) -> r) -> r
Costar f = HomF f Id
{-# COMPLETE Costar #-}

type x :*%: f = (x :*-: Cod f) :.: f
-- | The covariant functor Hom(X,F-)
pattern HomXF :: Functor f => Obj (Cod f) x -> f -> x :*%: f
pattern $bHomXF :: forall f x. Functor f => Obj (Cod f) x -> f -> x :*%: f
$mHomXF :: forall {r} {f} {x}.
Functor f =>
(x :*%: f) -> (Obj (Cod f) x -> f -> r) -> ((# #) -> r) -> r
HomXF x f = HomX_ x :.: f
{-# COMPLETE HomXF #-}

type f :%*: x = (Cod f :-*: x) :.: Opposite f
-- | The contravariant functor Hom(F-,X)
pattern HomFX :: Functor f => f -> Obj (Cod f) x -> f :%*: x
pattern $bHomFX :: forall f x. Functor f => f -> Obj (Cod f) x -> f :%*: x
$mHomFX :: forall {r} {f} {x}.
Functor f =>
(f :%*: x) -> (f -> Obj (Cod f) x -> r) -> ((# #) -> r) -> r
HomFX f x = Hom_X x :.: Opposite f
{-# COMPLETE HomFX #-}