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

import Data.Kind (Type)

import Data.Category (Category(..), Obj, Op(..))
import Data.Category.Product
import Data.Category.Functor (Functor(..), Hom(..))
import Data.Category.Limit (HasBinaryProducts(..), HasTerminalObject(..))
import Data.Category.CartesianClosed (CartesianClosed(..), ExpFunctor(..), curry, uncurry)

-- | An enriched category
class CartesianClosed (V k) => ECategory (k :: Type -> Type -> Type) where
  -- | The category V which k is enriched in
  type V k :: Type -> Type -> Type

  -- | The hom object in V from a to b
  type k $ ab :: Type
  hom :: Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))

  id :: Obj k a -> Arr k a a
  comp :: Obj k a -> Obj k b -> Obj k c -> V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))


-- | Arrows as elements of @k@
type Arr k a b = V k (TerminalObject (V k)) (k $ (a, b))

compArr :: ECategory k => Obj k a -> Obj k b -> Obj k c -> Arr k b c -> Arr k a b -> Arr k a c
compArr :: forall (k :: * -> * -> *) a b c.
ECategory k =>
Obj k a
-> Obj k b -> Obj k c -> Arr k b c -> Arr k a b -> Arr k a c
compArr Obj k a
a Obj k b
b Obj k c
c Arr k b c
f Arr k a b
g = 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 a
a Obj k b
b Obj k c
c forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Arr k b c
f 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)
&&& Arr k a b
g)


data Underlying k a b = Underlying (Obj k a) (Arr k a b) (Obj k b)
-- | The underlying category of an enriched category
instance ECategory k => Category (Underlying k) where
  src :: forall a b. Underlying k a b -> Obj (Underlying k) a
src (Underlying Obj k a
a Arr k a b
_ Obj k b
_) = forall (k :: * -> * -> *) a b.
Obj k a -> Arr k a b -> Obj k b -> Underlying k a b
Underlying Obj k a
a (forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id Obj k a
a) Obj k a
a
  tgt :: forall a b. Underlying k a b -> Obj (Underlying k) b
tgt (Underlying Obj k a
_ Arr k a b
_ Obj k b
b) = forall (k :: * -> * -> *) a b.
Obj k a -> Arr k a b -> Obj k b -> Underlying k a b
Underlying Obj k b
b (forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id Obj k b
b) Obj k b
b
  Underlying Obj k b
b Arr k b c
f Obj k c
c . :: forall b c a.
Underlying k b c -> Underlying k a b -> Underlying k a c
. Underlying Obj k a
a Arr k a b
g Obj k b
_ = forall (k :: * -> * -> *) a b.
Obj k a -> Arr k a b -> Obj k b -> Underlying k a b
Underlying Obj k a
a (forall (k :: * -> * -> *) a b c.
ECategory k =>
Obj k a
-> Obj k b -> Obj k c -> Arr k b c -> Arr k a b -> Arr k a c
compArr Obj k a
a Obj k b
b Obj k c
c Arr k b c
f Arr k a b
g) Obj k c
c


newtype EOp k a b = EOp (k b a)
-- | The opposite of an enriched category
instance ECategory k => ECategory (EOp k) where
  type V (EOp k) = V k
  type EOp k $ (a, b) = k $ (b, a)
  hom :: forall a b.
Obj (EOp k) a -> Obj (EOp k) b -> Obj (V (EOp k)) (EOp k $ (a, b))
hom (EOp k a a
a) (EOp k b b
b) = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom k b b
b k a a
a
  id :: forall a. Obj (EOp k) a -> Arr (EOp k) a a
id (EOp k a a
a) = forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id k a a
a
  comp :: forall a b c.
Obj (EOp k) a
-> Obj (EOp k) b
-> Obj (EOp k) c
-> V (EOp k)
     (BinaryProduct (V (EOp k)) (EOp k $ (b, c)) (EOp k $ (a, b)))
     (EOp k $ (a, c))
comp (EOp k a a
a) (EOp k b b
b) (EOp k c c
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 c c
c k b b
b k a a
a 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 (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom k c c
c k b b
b) (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom k b b
b k a a
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 (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom k c c
c k b b
b) (forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom k b b
b k a a
a))


data (:<>:) :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type where
  (:<>:) :: (V k1 ~ V k2) => Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)

-- | The enriched product category of enriched categories @c1@ and @c2@.
instance (ECategory k1, ECategory k2, V k1 ~ V k2) => ECategory (k1 :<>: k2) where
  type V (k1 :<>: k2) = V k1
  type (k1 :<>: k2) $ ((a1, a2), (b1, b2)) = BinaryProduct (V k1) (k1 $ (a1, b1)) (k2 $ (a2, b2))
  hom :: forall a b.
Obj (k1 :<>: k2) a
-> Obj (k1 :<>: k2) b
-> Obj (V (k1 :<>: k2)) ((k1 :<>: k2) $ (a, b))
hom (Obj k1 a1
a1 :<>: Obj k2 a2
a2) (Obj k1 a1
b1 :<>: Obj k2 a2
b2) = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k1 a1
a1 Obj k1 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 (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k2 a2
a2 Obj k2 a2
b2
  id :: forall a. Obj (k1 :<>: k2) a -> Arr (k1 :<>: k2) a a
id (Obj k1 a1
a1 :<>: Obj k2 a2
a2) = forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id Obj k1 a1
a1 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. ECategory k => Obj k a -> Arr k a a
id Obj k2 a2
a2
  comp :: forall a b c.
Obj (k1 :<>: k2) a
-> Obj (k1 :<>: k2) b
-> Obj (k1 :<>: k2) c
-> V (k1 :<>: k2)
     (BinaryProduct
        (V (k1 :<>: k2)) ((k1 :<>: k2) $ (b, c)) ((k1 :<>: k2) $ (a, b)))
     ((k1 :<>: k2) $ (a, c))
comp (Obj k1 a1
a1 :<>: Obj k2 a2
a2) (Obj k1 a1
b1 :<>: Obj k2 a2
b2) (Obj k1 a1
c1 :<>: Obj k2 a2
c2) =
    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 k1 a1
a1 Obj k1 a1
b1 Obj k1 a1
c1 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 k1) (k1 $ (a1, a1))
bc1 Obj (V k2) (k2 $ (a2, a2))
bc2 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 V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
l V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
r 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 k1) (k1 $ (a1, a1))
ab1 Obj (V k2) (k2 $ (a2, a2))
ab2 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 V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
l V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
r) 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 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 k2 a2
a2 Obj k2 a2
b2 Obj k2 a2
c2 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 k1) (k1 $ (a1, a1))
bc1 Obj (V k2) (k2 $ (a2, a2))
bc2 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 V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
l V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
r 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) y
proj2 Obj (V k1) (k1 $ (a1, a1))
ab1 Obj (V k2) (k2 $ (a2, a2))
ab2 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 V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
l V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
r)
    where
      ab1 :: Obj (V k1) (k1 $ (a1, a1))
ab1 = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k1 a1
a1 Obj k1 a1
b1
      ab2 :: Obj (V k2) (k2 $ (a2, a2))
ab2 = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k2 a2
a2 Obj k2 a2
b2
      bc1 :: Obj (V k1) (k1 $ (a1, a1))
bc1 = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k1 a1
b1 Obj k1 a1
c1
      bc2 :: Obj (V k2) (k2 $ (a2, a2))
bc2 = forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k2 a2
b2 Obj k2 a2
c2
      l :: V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
l = Obj (V k1) (k1 $ (a1, a1))
bc1 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 k2) (k2 $ (a2, a2))
bc2
      r :: V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
r = Obj (V k1) (k1 $ (a1, a1))
ab1 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 k2) (k2 $ (a2, a2))
ab2


newtype Self v a b = Self { forall (v :: * -> * -> *) a b. Self v a b -> v a b
getSelf :: v a b }
-- | Self enrichment
instance CartesianClosed v => ECategory (Self v) where
  type V (Self v) = v
  type Self v $ (a, b) = Exponential v a b
  hom :: forall a b.
Obj (Self v) a
-> Obj (Self v) b -> Obj (V (Self v)) (Self v $ (a, b))
hom (Self v a a
a) (Self v b b
b) = forall (k :: * -> * -> *). ExpFunctor k
ExpFunctor forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op v a a
a forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: v b b
b)
  id :: forall a. Obj (Self v) a -> Arr (Self v) a a
id (Self v a a
a) = forall (v :: * -> * -> *) a b.
CartesianClosed v =>
v a b -> Arr (Self v) a b
toSelf v a a
a
  comp :: forall a b c.
Obj (Self v) a
-> Obj (Self v) b
-> Obj (Self v) c
-> V (Self v)
     (BinaryProduct (V (Self v)) (Self v $ (b, c)) (Self v $ (a, b)))
     (Self v $ (a, c))
comp (Self v a a
a) (Self v b b
b) (Self v c c
c) = 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 (v (Exponential v b c) (Exponential v b c)
bc 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)
*** v (Exponential v a b) (Exponential v a b)
ab) v a a
a v c c
c (forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
apply v b b
b v c c
c 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 v (Exponential v b c) (Exponential v b c)
bc v (Exponential v a b) (Exponential v a b)
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)
*** forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
apply v a a
a v b b
b) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. v (BinaryProduct
     v (BinaryProduct v (Exponential v b c) (Exponential v a b)) a)
  (BinaryProduct
     v
     (BinaryProduct v (Exponential v b c) (Exponential v a b))
     (BinaryProduct v (Exponential v a b) a))
shuffle)
    where
      bc :: v (Exponential v b c) (Exponential v b c)
bc = v c c
c forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ v b b
b
      ab :: v (Exponential v a b) (Exponential v a b)
ab = v b b
b forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ v a a
a
      shuffle :: v (BinaryProduct
     v (BinaryProduct v (Exponential v b c) (Exponential v a b)) a)
  (BinaryProduct
     v
     (BinaryProduct v (Exponential v b c) (Exponential v a b))
     (BinaryProduct v (Exponential v a b) a))
shuffle = forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 (v (Exponential v b c) (Exponential v b c)
bc 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)
*** v (Exponential v a b) (Exponential v a b)
ab) v a a
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) y
proj2 v (Exponential v b c) (Exponential v b c)
bc v (Exponential v a b) (Exponential v a b)
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)
*** v a a
a)

toSelf :: CartesianClosed v => v a b -> Arr (Self v) a b
toSelf :: forall (v :: * -> * -> *) a b.
CartesianClosed v =>
v a b -> Arr (Self v) a b
toSelf v a b
v = 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} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src v a b
v) (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt v a b
v) (v a b
v 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 forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src v a b
v))

fromSelf :: forall v a b. CartesianClosed v => Obj v a -> Obj v b -> Arr (Self v) a b -> v a b
fromSelf :: forall (v :: * -> * -> *) a b.
CartesianClosed v =>
Obj v a -> Obj v b -> Arr (Self v) a b -> v a b
fromSelf Obj v a
a Obj v b
b Arr (Self v) a b
arr = 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 forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject Obj v a
a Obj v b
b Arr (Self v) a b
arr 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 Obj v a
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)
&&& Obj v a
a)


newtype InHask k a b = InHask (k a b)
-- | Any regular category is enriched in (->), aka Hask
instance Category k => ECategory (InHask k) where
  type V (InHask k) = (->)
  type InHask k $ (a, b) = k a b
  hom :: forall a b.
Obj (InHask k) a
-> Obj (InHask k) b -> Obj (V (InHask k)) (InHask k $ (a, b))
hom (InHask k a a
a) (InHask k b b
b) = forall (k :: * -> * -> *). Hom k
Hom forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op k a a
a forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: k b b
b)
  id :: forall a. Obj (InHask k) a -> Arr (InHask k) a a
id (InHask k a a
f) () = k a a
f
  comp :: forall a b c.
Obj (InHask k) a
-> Obj (InHask k) b
-> Obj (InHask k) c
-> V (InHask k)
     (BinaryProduct
        (V (InHask k)) (InHask k $ (b, c)) (InHask k $ (a, b)))
     (InHask k $ (a, c))
comp Obj (InHask k) a
_ Obj (InHask k) b
_ Obj (InHask k) c
_ (k b c
f, k a b
g) = k b c
f forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k a b
g