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

import Data.Kind (Type)

import Data.Category (Category(..), Obj)
import Data.Category.Functor (Functor(..))
import Data.Category.Limit (HasBinaryProducts(..), HasTerminalObject(..))
import Data.Category.CartesianClosed
import Data.Category.Enriched

-- | Enriched functors.
class (ECategory (EDom ftag), ECategory (ECod ftag), V (EDom ftag) ~ V (ECod ftag)) => EFunctor ftag where

  -- | The domain, or source category, of the functor.
  type EDom ftag :: Type -> Type -> Type
  -- | The codomain, or target category, of the functor.
  type ECod ftag :: Type -> Type -> Type

  -- | @:%%@ maps objects at the type level
  type ftag :%% a :: Type

  -- | @%%@ maps object at the value level
  (%%) :: ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)

  -- | `map` maps arrows.
  map :: (EDom ftag ~ k) => ftag -> Obj k a -> Obj k b -> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))

type EFunctorOf a b t = (EFunctor t, EDom t ~ a, ECod t ~ b)


data Id (k :: Type -> Type -> Type) = Id
-- | The identity functor on k
instance ECategory k => EFunctor (Id k) where
  type EDom (Id k) = k
  type ECod (Id k) = k
  type Id k :%% a = a
  Id k
Id %% :: forall a.
Id k -> Obj (EDom (Id k)) a -> Obj (ECod (Id k)) (Id k :%% a)
%% Obj (EDom (Id k)) a
a = Obj (EDom (Id k)) a
a
  map :: forall (k :: * -> * -> *) a b.
(EDom (Id k) ~ k) =>
Id k
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod (Id k) $ (Id k :%% a, Id k :%% b))
map Id k
Id = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom

data (g :.: h) where
  (:.:) :: (EFunctor g, EFunctor h, ECod h ~ EDom g) => g -> h -> g :.: h
-- | The composition of two functors.
instance (ECategory (ECod g), ECategory (EDom h), V (EDom h) ~ V (ECod g), ECod h ~ EDom g) => EFunctor (g :.: h) where
  type EDom (g :.: h) = EDom h
  type ECod (g :.: h) = ECod g
  type (g :.: h) :%% a = g :%% (h :%% a)
  (g
g :.: h
h) %% :: forall a.
(g :.: h)
-> Obj (EDom (g :.: h)) a -> Obj (ECod (g :.: h)) ((g :.: h) :%% a)
%% Obj (EDom (g :.: h)) a
a = g
g forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% (h
h forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom (g :.: h)) a
a)
  map :: forall (k :: * -> * -> *) a b.
(EDom (g :.: h) ~ k) =>
(g :.: h)
-> Obj k a
-> Obj k b
-> V k
     (k $ (a, b))
     (ECod (g :.: h) $ ((g :.: h) :%% a, (g :.: h) :%% b))
map (g
g :.: h
h) Obj k a
a Obj k b
b = forall ftag (k :: * -> * -> *) a b.
(EFunctor ftag, EDom ftag ~ k) =>
ftag
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
map g
g (h
h forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj k a
a) (h
h forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj k b
b) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall ftag (k :: * -> * -> *) a b.
(EFunctor ftag, EDom ftag ~ k) =>
ftag
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
map h
h Obj k a
a Obj k b
b

data Const (c1 :: Type -> Type -> Type) (c2 :: Type -> Type -> Type) x where
  Const :: Obj c2 x -> Const c1 c2 x
-- | The constant functor.
instance (ECategory c1, ECategory c2, V c1 ~ V c2) => EFunctor (Const c1 c2 x) where
  type EDom (Const c1 c2 x) = c1
  type ECod (Const c1 c2 x) = c2
  type Const c1 c2 x :%% a = x
  Const Obj c2 x
x %% :: forall a.
Const c1 c2 x
-> Obj (EDom (Const c1 c2 x)) a
-> Obj (ECod (Const c1 c2 x)) (Const c1 c2 x :%% a)
%% Obj (EDom (Const c1 c2 x)) a
_ = Obj c2 x
x
  map :: forall (k :: * -> * -> *) a b.
(EDom (Const c1 c2 x) ~ k) =>
Const c1 c2 x
-> Obj k a
-> Obj k b
-> V k
     (k $ (a, b))
     (ECod (Const c1 c2 x) $ (Const c1 c2 x :%% a, Const c1 c2 x :%% b))
map (Const Obj c2 x
x) Obj k a
a Obj k b
b = forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id Obj c2 x
x forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k a
a Obj k b
b)

data Opposite f where
  Opposite :: EFunctor f => f -> Opposite f
-- | The dual of a functor
instance (EFunctor f) => EFunctor (Opposite f) where
  type EDom (Opposite f) = EOp (EDom f)
  type ECod (Opposite f) = EOp (ECod f)
  type Opposite f :%% a = f :%% a
  Opposite f
f %% :: forall a.
Opposite f
-> Obj (EDom (Opposite f)) a
-> Obj (ECod (Opposite f)) (Opposite f :%% a)
%% EOp EDom f a a
a = forall (k :: * -> * -> *) a b. k b a -> EOp k a b
EOp (f
f forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% EDom f a a
a)
  map :: forall (k :: * -> * -> *) a b.
(EDom (Opposite f) ~ k) =>
Opposite f
-> Obj k a
-> Obj k b
-> V k
     (k $ (a, b))
     (ECod (Opposite f) $ (Opposite f :%% a, Opposite f :%% b))
map (Opposite f
f) (EOp EDom f a a
a) (EOp EDom f b b
b) = forall ftag (k :: * -> * -> *) a b.
(EFunctor ftag, EDom ftag ~ k) =>
ftag
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
map f
f EDom f b b
b EDom f a a
a

data f1 :<*>: f2 = f1 :<*>: f2
-- | @f1 :<*>: f2@ is the product of the functors @f1@ and @f2@.
instance (EFunctor f1, EFunctor f2, V (ECod f1) ~ V (ECod f2)) => EFunctor (f1 :<*>: f2) where
  type EDom (f1 :<*>: f2) = EDom f1 :<>: EDom f2
  type ECod (f1 :<*>: f2) = ECod f1 :<>: ECod f2
  type (f1 :<*>: f2) :%% (a1, a2) = (f1 :%% a1, f2 :%% a2)
  (f1
f1 :<*>: f2
f2) %% :: forall a.
(f1 :<*>: f2)
-> Obj (EDom (f1 :<*>: f2)) a
-> Obj (ECod (f1 :<*>: f2)) ((f1 :<*>: f2) :%% a)
%% (Obj (EDom f1) a1
a1 :<>: Obj (EDom f2) a2
a2) = (f1
f1 forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom f1) a1
a1) forall (k1 :: * -> * -> *) (k2 :: * -> * -> *) a1 a2.
(V k1 ~ V k2) =>
Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
:<>: (f2
f2 forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom f2) a2
a2)
  map :: forall (k :: * -> * -> *) a b.
(EDom (f1 :<*>: f2) ~ k) =>
(f1 :<*>: f2)
-> Obj k a
-> Obj k b
-> V k
     (k $ (a, b))
     (ECod (f1 :<*>: f2) $ ((f1 :<*>: f2) :%% a, (f1 :<*>: f2) :%% b))
map (f1
f1 :<*>: f2
f2) (Obj (EDom f1) a1
a1 :<>: Obj (EDom f2) a2
a2) (Obj (EDom f1) a1
b1 :<>: Obj (EDom f2) a2
b2) = forall ftag (k :: * -> * -> *) a b.
(EFunctor ftag, EDom ftag ~ k) =>
ftag
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
map f1
f1 Obj (EDom f1) a1
a1 Obj (EDom f1) a1
b1 forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** forall ftag (k :: * -> * -> *) a b.
(EFunctor ftag, EDom ftag ~ k) =>
ftag
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
map f2
f2 Obj (EDom f2) a2
a2 Obj (EDom f2) a2
b2

data DiagProd (k :: Type -> Type -> Type) = DiagProd
-- | 'DiagProd' is the diagonal functor for products.
instance ECategory k => EFunctor (DiagProd k) where
  type EDom (DiagProd k) = k
  type ECod (DiagProd k) = k :<>: k
  type DiagProd k :%% a = (a, a)
  DiagProd k
DiagProd %% :: forall a.
DiagProd k
-> Obj (EDom (DiagProd k)) a
-> Obj (ECod (DiagProd k)) (DiagProd k :%% a)
%% Obj (EDom (DiagProd k)) a
a = Obj (EDom (DiagProd k)) a
a forall (k1 :: * -> * -> *) (k2 :: * -> * -> *) a1 a2.
(V k1 ~ V k2) =>
Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
:<>: Obj (EDom (DiagProd k)) a
a
  map :: forall (k :: * -> * -> *) a b.
(EDom (DiagProd k) ~ k) =>
DiagProd k
-> Obj k a
-> Obj k b
-> V k
     (k $ (a, b))
     (ECod (DiagProd k) $ (DiagProd k :%% a, DiagProd k :%% b))
map DiagProd k
DiagProd Obj k a
a Obj k b
b = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k a
a Obj k b
b forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k a
a Obj k b
b

newtype UnderlyingF f = UnderlyingF f
-- | The underlying functor of an enriched functor @f@
instance EFunctor f => Functor (UnderlyingF f) where
  type Dom (UnderlyingF f) = Underlying (EDom f)
  type Cod (UnderlyingF f) = Underlying (ECod f)
  type UnderlyingF f :% a = f :%% a
  UnderlyingF f
f % :: forall a b.
UnderlyingF f
-> Dom (UnderlyingF f) a b
-> Cod (UnderlyingF f) (UnderlyingF f :% a) (UnderlyingF f :% b)
% Underlying Obj (EDom f) a
a Arr (EDom f) a b
ab Obj (EDom f) b
b = forall (k :: * -> * -> *) a b.
Obj k a -> Arr k a b -> Obj k b -> Underlying k a b
Underlying (f
f forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom f) a
a) (forall ftag (k :: * -> * -> *) a b.
(EFunctor ftag, EDom ftag ~ k) =>
ftag
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
map f
f Obj (EDom f) a
a Obj (EDom f) b
b forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Arr (EDom f) a b
ab) (f
f forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom f) b
b)

newtype InHaskF f = InHaskF f
-- | A regular functor is a functor enriched in Hask.
instance Functor f => EFunctor (InHaskF f) where
  type EDom (InHaskF f) = InHask (Dom f)
  type ECod (InHaskF f) = InHask (Cod f)
  type InHaskF f :%% a = f :% a
  InHaskF f
f %% :: forall a.
InHaskF f
-> Obj (EDom (InHaskF f)) a
-> Obj (ECod (InHaskF f)) (InHaskF f :%% a)
%% InHask Dom f a a
a = forall (k :: * -> * -> *) a b. k a b -> InHask k a b
InHask (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f a a
a)
  map :: forall (k :: * -> * -> *) a b.
(EDom (InHaskF f) ~ k) =>
InHaskF f
-> Obj k a
-> Obj k b
-> V k
     (k $ (a, b))
     (ECod (InHaskF f) $ (InHaskF f :%% a, InHaskF f :%% b))
map (InHaskF f
f) Obj k a
_ Obj k b
_ = \Dom f a b
g -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f a b
g

newtype InHaskToHask f = InHaskToHask f
instance (Functor f, Cod f ~ (->)) => EFunctor (InHaskToHask f) where
  type EDom (InHaskToHask f) = InHask (Dom f)
  type ECod (InHaskToHask f) = Self (->)
  type InHaskToHask f :%% a = f :% a
  InHaskToHask f
f %% :: forall a.
InHaskToHask f
-> Obj (EDom (InHaskToHask f)) a
-> Obj (ECod (InHaskToHask f)) (InHaskToHask f :%% a)
%% InHask Dom f a a
a = forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f a a
a)
  map :: forall (k :: * -> * -> *) a b.
(EDom (InHaskToHask f) ~ k) =>
InHaskToHask f
-> Obj k a
-> Obj k b
-> V k
     (k $ (a, b))
     (ECod (InHaskToHask f)
      $ (InHaskToHask f :%% a, InHaskToHask f :%% b))
map (InHaskToHask f
f) Obj k a
_ Obj k b
_ = \Dom f a b
g -> f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom f a b
g

newtype UnderlyingHask (c :: Type -> Type -> Type) (d :: Type -> Type -> Type) f = UnderlyingHask f
-- | The underlying functor of an enriched functor @f@ enriched in Hask.
instance (EFunctor f, EDom f ~ InHask c, ECod f ~ InHask d, Category c, Category d) => Functor (UnderlyingHask c d f) where
  type Dom (UnderlyingHask c d f) = c
  type Cod (UnderlyingHask c d f) = d
  type UnderlyingHask c d f :% a = f :%% a
  UnderlyingHask f
f % :: forall a b.
UnderlyingHask c d f
-> Dom (UnderlyingHask c d f) a b
-> Cod
     (UnderlyingHask c d f)
     (UnderlyingHask c d f :% a)
     (UnderlyingHask c d f :% b)
% Dom (UnderlyingHask c d f) a b
g = forall ftag (k :: * -> * -> *) a b.
(EFunctor ftag, EDom ftag ~ k) =>
ftag
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
map f
f (forall (k :: * -> * -> *) a b. k a b -> InHask k a b
InHask (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Dom (UnderlyingHask c d f) a b
g)) (forall (k :: * -> * -> *) a b. k a b -> InHask k a b
InHask (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Dom (UnderlyingHask c d f) a b
g)) Dom (UnderlyingHask c d f) a b
g

data EHom (k :: Type -> Type -> Type) = EHom
instance ECategory k => EFunctor (EHom k) where
  type EDom (EHom k) = EOp k :<>: k
  type ECod (EHom k) = Self (V k)
  type EHom k :%% (a, b) = k $ (a, b)
  EHom k
EHom %% :: forall a.
EHom k
-> Obj (EDom (EHom k)) a -> Obj (ECod (EHom k)) (EHom k :%% a)
%% (EOp k a1 a1
a :<>: Obj k a2
b) = forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom k a1 a1
a Obj k a2
b)
  map :: forall (k :: * -> * -> *) a b.
(EDom (EHom k) ~ k) =>
EHom k
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod (EHom k) $ (EHom k :%% a, EHom k :%% b))
map EHom k
EHom (EOp k a1 a1
a1 :<>: Obj k a2
a2) (EOp k a1 a1
b1 :<>: Obj k a2
b2) = forall {k1} (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, Kind k2 ~ *) =>
Obj k2 x
-> Obj k2 y
-> Obj k2 z
-> k2 (BinaryProduct k2 x y) z
-> k2 x (Exponential k2 y z)
curry (Obj (V k) (k $ (a1, a1))
ba forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj (V k) (k $ (a2, a2))
ab) Obj (V k) (k $ (a1, a2))
a Obj (V k) (k $ (a1, a2))
b (forall (k :: * -> * -> *) a b c.
ECategory k =>
Obj k a
-> Obj k b
-> Obj k c
-> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))
comp k a1 a1
b1 k a1 a1
a1 Obj k a2
b2 forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (forall (k :: * -> * -> *) a b c.
ECategory k =>
Obj k a
-> Obj k b
-> Obj k c
-> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))
comp k a1 a1
a1 Obj k a2
a2 Obj k a2
b2 forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj (V k) (k $ (a1, a1))
ba Obj (V k) (k $ (a2, a2))
ab forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj (V k) (k $ (a1, a2))
a) forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj (V k) (k $ (a1, a1))
ba Obj (V k) (k $ (a2, a2))
ab forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 (Obj (V k) (k $ (a1, a1))
ba forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj (V k) (k $ (a2, a2))
ab) Obj (V k) (k $ (a1, a2))
a))
    where
      a :: Obj (V k) (k $ (a1, a2))
a = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom k a1 a1
a1 Obj k a2
a2
      b :: Obj (V k) (k $ (a1, a2))
b = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom k a1 a1
b1 Obj k a2
b2
      ba :: Obj (V k) (k $ (a1, a1))
ba = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom k a1 a1
b1 k a1 a1
a1
      ab :: Obj (V k) (k $ (a2, a2))
ab = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k a2
a2 Obj k a2
b2

-- | The enriched functor @k(x, -)@
data EHomX_ k x = EHomX_ (Obj k x)
instance ECategory k => EFunctor (EHomX_ k x) where
  type EDom (EHomX_ k x) = k
  type ECod (EHomX_ k x) = Self (V k)
  type EHomX_ k x :%% y = k $ (x, y)
  EHomX_ Obj k x
x %% :: forall a.
EHomX_ k x
-> Obj (EDom (EHomX_ k x)) a
-> Obj (ECod (EHomX_ k x)) (EHomX_ k x :%% a)
%% Obj (EDom (EHomX_ k x)) a
y = forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k x
x Obj (EDom (EHomX_ k x)) a
y)
  map :: forall (k :: * -> * -> *) a b.
(EDom (EHomX_ k x) ~ k) =>
EHomX_ k x
-> Obj k a
-> Obj k b
-> V k
     (k $ (a, b))
     (ECod (EHomX_ k x) $ (EHomX_ k x :%% a, EHomX_ k x :%% b))
map (EHomX_ Obj k x
x) Obj k a
a Obj k b
b = forall {k1} (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, Kind k2 ~ *) =>
Obj k2 x
-> Obj k2 y
-> Obj k2 z
-> k2 (BinaryProduct k2 x y) z
-> k2 x (Exponential k2 y z)
curry (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k a
a Obj k b
b) (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k x
x Obj k a
a) (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k x
x Obj k b
b) (forall (k :: * -> * -> *) a b c.
ECategory k =>
Obj k a
-> Obj k b
-> Obj k c
-> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))
comp Obj k x
x Obj k a
a Obj k b
b)

-- | The enriched functor @k(-, x)@
data EHom_X k x = EHom_X (Obj (EOp k) x)
instance ECategory k => EFunctor (EHom_X k x) where
  type EDom (EHom_X k x) = EOp k
  type ECod (EHom_X k x) = Self (V k)
  type EHom_X k x :%% y = k $ (y, x)
  EHom_X Obj (EOp k) x
x %% :: forall a.
EHom_X k x
-> Obj (EDom (EHom_X k x)) a
-> Obj (ECod (EHom_X k x)) (EHom_X k x :%% a)
%% Obj (EDom (EHom_X k x)) a
y = forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj (EOp k) x
x Obj (EDom (EHom_X k x)) a
y)
  map :: forall (k :: * -> * -> *) a b.
(EDom (EHom_X k x) ~ k) =>
EHom_X k x
-> Obj k a
-> Obj k b
-> V k
     (k $ (a, b))
     (ECod (EHom_X k x) $ (EHom_X k x :%% a, EHom_X k x :%% b))
map (EHom_X Obj (EOp k) x
x) Obj k a
a Obj k b
b = forall {k1} (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, Kind k2 ~ *) =>
Obj k2 x
-> Obj k2 y
-> Obj k2 z
-> k2 (BinaryProduct k2 x y) z
-> k2 x (Exponential k2 y z)
curry (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k a
a Obj k b
b) (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj (EOp k) x
x Obj k a
a) (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj (EOp k) x
x Obj k b
b) (forall (k :: * -> * -> *) a b c.
ECategory k =>
Obj k a
-> Obj k b
-> Obj k c
-> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))
comp Obj (EOp k) x
x Obj k a
a Obj k b
b)


-- | A V-enrichment on a functor @F: V -> V@ is the same thing as tensorial strength @(a, f b) -> f (a, b)@.
strength :: EFunctorOf (Self v) (Self v) f => f -> Obj v a -> Obj v b -> v (BinaryProduct v a (f :%% b)) (f :%% (BinaryProduct v a b))
strength :: forall (v :: * -> * -> *) f a b.
EFunctorOf (Self v) (Self v) f =>
f
-> Obj v a
-> Obj v b
-> v (BinaryProduct v a (f :%% b)) (f :%% BinaryProduct v a b)
strength f
f Obj v a
a Obj v b
b = forall {k1} (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, Kind k2 ~ *) =>
Obj k2 x
-> Obj k2 y
-> Obj k2 z
-> k2 x (Exponential k2 y z)
-> k2 (BinaryProduct k2 x y) z
uncurry Obj v a
a v (f :%% b) (f :%% b)
fb v (f :%% BinaryProduct v a b) (f :%% BinaryProduct v a b)
fab (forall ftag (k :: * -> * -> *) a b.
(EFunctor ftag, EDom ftag ~ k) =>
ftag
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod ftag $ (ftag :%% a, ftag :%% b))
map f
f (forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self Obj v b
b) (forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (Obj v a
a forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj v b
b)) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
tuple Obj v b
b Obj v a
a)
  where
    Self v (f :%% b) (f :%% b)
fb = f
f forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self Obj v b
b
    Self v (f :%% BinaryProduct v a b) (f :%% BinaryProduct v a b)
fab = f
f forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (Obj v a
a forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj v b
b)


-- | Enriched natural transformations.
data ENat :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where
  ENat :: (EFunctorOf c d f, EFunctorOf c d g)
    => f -> g -> (forall z. Obj c z -> Arr d (f :%% z) (g :%% z)) -> ENat c d f g