{-# LANGUAGE
    TypeOperators
  , TypeFamilies
  , GADTs
  , RankNTypes
  , PatternSynonyms
  , FlexibleContexts
  , NoImplicitPrelude
  , UndecidableInstances
  , ScopedTypeVariables
  , ConstraintKinds
  , AllowAmbiguousTypes
  , TypeApplications
  #-}
-----------------------------------------------------------------------------
-- |
-- 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.Category (Category(..), Obj, Op(..))
import Data.Category.Product
import Data.Category.Functor (Functor(..), Hom(..), (:*-:), pattern HomX_)
import Data.Category.Limit hiding (HasLimits)
import Data.Category.CartesianClosed
import Data.Category.Boolean


-- | An enriched category
class CartesianClosed (V k) => ECategory (k :: * -> * -> *) where
  -- | The tensor product of the category V which k is enriched in
  type V k :: * -> * -> *

  -- | The hom object in V from a to b
  type k $ ab :: *
  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))


-- | The elements of @k@ as a functor from @V k@ to @(->)@ 
type Elem k = TerminalObject (V k) :*-: (V k)
elem :: CartesianClosed (V k) => Elem k
elem :: Elem k
elem = Obj (V k) (TerminalObject (V k)) -> Elem k
forall (k :: * -> * -> *) x. Category k => Obj k x -> x :*-: k
HomX_ Obj (V k) (TerminalObject (V k))
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject

-- | Arrows as elements of @k@
type Arr k a b = Elem 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 :: 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 a
-> Obj k b
-> Obj k c
-> V k (BinaryProduct (V 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 Obj k a
a Obj k b
b Obj k c
c V k (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b))) (k $ (a, c))
-> V k
     (TerminalObject (V k))
     (BinaryProduct (V k) (k $ (b, c)) (k $ (a, b)))
-> V k (TerminalObject (V k)) (k $ (a, 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
V k (TerminalObject (V k)) (k $ (b, c))
f V k (TerminalObject (V k)) (k $ (b, c))
-> V k (TerminalObject (V k)) (k $ (a, b))
-> V k
     (TerminalObject (V k))
     (BinaryProduct (V k) (k $ (b, c)) (k $ (a, 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)
&&& Arr k a b
V k (TerminalObject (V k)) (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 :: Underlying k a b -> Obj (Underlying k) a
src (Underlying Obj k a
a Arr k a b
_ Obj k b
_) = Obj k a -> Arr k a a -> Obj k a -> Obj (Underlying k) a
forall (k :: * -> * -> *) a b.
Obj k a -> Arr k a b -> Obj k b -> Underlying k a b
Underlying Obj k a
a (Obj k a -> Arr 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 :: Underlying k a b -> Obj (Underlying k) b
tgt (Underlying Obj k a
_ Arr k a b
_ Obj k b
b) = Obj k b -> Arr k b b -> Obj k b -> Obj (Underlying k) b
forall (k :: * -> * -> *) a b.
Obj k a -> Arr k a b -> Obj k b -> Underlying k a b
Underlying Obj k b
b (Obj k b -> Arr 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 . :: 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
_ = Obj k a -> Arr k a c -> Obj k c -> Underlying k a c
forall (k :: * -> * -> *) a b.
Obj k a -> Arr k a b -> Obj k b -> Underlying k a b
Underlying Obj k a
a (Obj k a
-> Obj k b -> Obj k c -> Arr k b c -> Arr k a b -> Arr k a c
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 :: 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) = k b b -> k a a -> Obj (V k) (k $ (b, a))
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 :: Obj (EOp k) a -> Arr (EOp k) a a
id (EOp k a a
a) = k a a -> Arr k a a
forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id k a a
a
  comp :: 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) = k c c
-> k b b
-> k a a
-> V k (BinaryProduct (V k) (k $ (b, a)) (k $ (c, b))) (k $ (c, a))
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 V k (BinaryProduct (V k) (k $ (b, a)) (k $ (c, b))) (k $ (c, a))
-> V k
     (BinaryProduct (V k) (k $ (c, b)) (k $ (b, a)))
     (BinaryProduct (V k) (k $ (b, a)) (k $ (c, b)))
-> V k (BinaryProduct (V k) (k $ (c, b)) (k $ (b, a))) (k $ (c, a))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Obj (V k) (k $ (c, b))
-> Obj (V k) (k $ (b, a))
-> V k (BinaryProduct (V k) (k $ (c, b)) (k $ (b, a))) (k $ (b, a))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 (k c c -> k b b -> Obj (V k) (k $ (c, b))
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) (k b b -> k a a -> Obj (V k) (k $ (b, a))
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) V k (BinaryProduct (V k) (k $ (c, b)) (k $ (b, a))) (k $ (b, a))
-> V k (BinaryProduct (V k) (k $ (c, b)) (k $ (b, a))) (k $ (c, b))
-> V k
     (BinaryProduct (V k) (k $ (c, b)) (k $ (b, a)))
     (BinaryProduct (V k) (k $ (b, a)) (k $ (c, 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)
&&& Obj (V k) (k $ (c, b))
-> Obj (V k) (k $ (b, a))
-> V k (BinaryProduct (V k) (k $ (c, b)) (k $ (b, a))) (k $ (c, b))
forall k (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 (k c c -> k b b -> Obj (V k) (k $ (c, b))
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) (k b b -> k a a -> Obj (V k) (k $ (b, a))
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 (:<>:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * 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 :: 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) = Obj k1 a1 -> Obj k1 a1 -> Obj (V k1) (k1 $ (a1, a1))
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 V k2 (k1 $ (a1, a1)) (k1 $ (a1, a1))
-> V k2 (k2 $ (a2, a2)) (k2 $ (a2, a2))
-> V k2
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
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 k2 a2 -> Obj k2 a2 -> V k2 (k2 $ (a2, a2)) (k2 $ (a2, a2))
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 :: Obj (k1 :<>: k2) a -> Arr (k1 :<>: k2) a a
id (Obj k1 a1
a1 :<>: Obj k2 a2
a2) = Obj k1 a1 -> Arr k1 a1 a1
forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id Obj k1 a1
a1 V k2 (TerminalObject (V k2)) (k1 $ (a1, a1))
-> V k2 (TerminalObject (V k2)) (k2 $ (a2, a2))
-> V k2
     (TerminalObject (V k2))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
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 k2 a2 -> Arr k2 a2 a2
forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id Obj k2 a2
a2
  comp :: 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) = 
    Obj k1 a1
-> Obj k1 a1
-> Obj k1 a1
-> V k1
     (BinaryProduct (V k1) (k1 $ (a1, a1)) (k1 $ (a1, a1)))
     (k1 $ (a1, a1))
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 V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k1 $ (a1, a1)))
  (k1 $ (a1, a1))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k1 $ (a1, a1)))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (k1 $ (a1, a1))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Obj (V k2) (k1 $ (a1, a1))
-> Obj (V k2) (k2 $ (a2, a2))
-> V k2
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
     (k1 $ (a1, a1))
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))
Obj (V k2) (k1 $ (a1, a1))
bc1 Obj (V k2) (k2 $ (a2, a2))
bc2 V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (k1 $ (a1, a1))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (k1 $ (a1, a1))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> Obj
     (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
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 k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
l Obj (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
r V k2
  (BinaryProduct
     (V k2)
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
  (k1 $ (a1, a1))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (k1 $ (a1, a1))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (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)
&&& Obj (V k2) (k1 $ (a1, a1))
-> Obj (V k2) (k2 $ (a2, a2))
-> V k2
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
     (k1 $ (a1, a1))
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))
Obj (V k2) (k1 $ (a1, a1))
ab1 Obj (V k2) (k2 $ (a2, a2))
ab2 V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (k1 $ (a1, a1))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (k1 $ (a1, a1))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> Obj
     (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
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 k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
l Obj (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
r) V k2
  (BinaryProduct
     (V k2)
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
  (k1 $ (a1, a1))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (k2 $ (a2, a2))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
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 k2 a2
-> Obj k2 a2
-> Obj k2 a2
-> V k2
     (BinaryProduct (V k2) (k2 $ (a2, a2)) (k2 $ (a2, a2)))
     (k2 $ (a2, a2))
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 V k2
  (BinaryProduct (V k2) (k2 $ (a2, a2)) (k2 $ (a2, a2)))
  (k2 $ (a2, a2))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k2 $ (a2, a2)) (k2 $ (a2, a2)))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (k2 $ (a2, a2))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Obj (V k2) (k1 $ (a1, a1))
-> Obj (V k2) (k2 $ (a2, a2))
-> V k2
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
     (k2 $ (a2, a2))
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))
Obj (V k2) (k1 $ (a1, a1))
bc1 Obj (V k2) (k2 $ (a2, a2))
bc2 V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (k2 $ (a2, a2))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (k2 $ (a2, a2))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> Obj
     (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
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 k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
l Obj (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
r V k2
  (BinaryProduct
     (V k2)
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
  (k2 $ (a2, a2))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (k2 $ (a2, a2))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k2 $ (a2, a2)) (k2 $ (a2, a2)))
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 k2) (k1 $ (a1, a1))
-> Obj (V k2) (k2 $ (a2, a2))
-> V k2
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
     (k2 $ (a2, a2))
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))
Obj (V k2) (k1 $ (a1, a1))
ab1 Obj (V k2) (k2 $ (a2, a2))
ab2 V k2
  (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
  (k2 $ (a2, a2))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (k2 $ (a2, a2))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> Obj
     (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
-> V k2
     (BinaryProduct
        (V k2)
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
        (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2))))
     (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
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 k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
l Obj (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
r)
    where 
      ab1 :: Obj (V k1) (k1 $ (a1, a1))
ab1 = Obj k1 a1 -> Obj k1 a1 -> Obj (V k1) (k1 $ (a1, a1))
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 = Obj k2 a2 -> Obj k2 a2 -> Obj (V k2) (k2 $ (a2, a2))
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 = Obj k1 a1 -> Obj k1 a1 -> Obj (V k1) (k1 $ (a1, a1))
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 = Obj k2 a2 -> Obj k2 a2 -> Obj (V k2) (k2 $ (a2, a2))
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 :: Obj (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
l = Obj (V k1) (k1 $ (a1, a1))
Obj (V k2) (k1 $ (a1, a1))
bc1 Obj (V k2) (k1 $ (a1, a1))
-> Obj (V k2) (k2 $ (a2, a2))
-> Obj
     (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
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 :: Obj (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
r = Obj (V k1) (k1 $ (a1, a1))
Obj (V k2) (k1 $ (a1, a1))
ab1 Obj (V k2) (k1 $ (a1, a1))
-> Obj (V k2) (k2 $ (a2, a2))
-> Obj
     (V k2) (BinaryProduct (V k2) (k1 $ (a1, a1)) (k2 $ (a2, a2)))
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 { 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 :: 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) = ExpFunctor v
forall (k :: * -> * -> *). ExpFunctor k
ExpFunctor ExpFunctor v
-> Dom (ExpFunctor v) (a, b) (a, b)
-> Cod
     (ExpFunctor v) (ExpFunctor v :% (a, b)) (ExpFunctor v :% (a, b))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (v a a -> Op v a a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op v a a
a Op v a a -> v b b -> (:**:) (Op v) v (a, b) (a, b)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: v b b
b)
  id :: Obj (Self v) a -> Arr (Self v) a a
id (Self v a a
a) = v a a -> Arr (Self v) a a
forall (v :: * -> * -> *) a b.
CartesianClosed v =>
v a b -> Arr (Self v) a b
toSelf v a a
a
  comp :: 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) = Obj v (BinaryProduct v (Exponential v b c) (Exponential v a b))
-> v a a
-> v c c
-> v (BinaryProduct
        v (BinaryProduct v (Exponential v b c) (Exponential v a b)) a)
     c
-> v (BinaryProduct v (Exponential v b c) (Exponential v a b))
     (Exponential v a c)
forall k1 (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, k1 ~ *) =>
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 v (Exponential v b c) (Exponential v b c)
-> v (Exponential v a b) (Exponential v a b)
-> Obj v (BinaryProduct v (Exponential v b c) (Exponential v a b))
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 (v b b -> v c c -> v (BinaryProduct v (Exponential v b c) b) 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 v (BinaryProduct v (Exponential v b c) b) c
-> v (BinaryProduct
        v (BinaryProduct v (Exponential v b c) (Exponential v a b)) a)
     (BinaryProduct v (Exponential v b c) b)
-> v (BinaryProduct
        v (BinaryProduct v (Exponential v b c) (Exponential v a b)) a)
     c
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (v (Exponential v b c) (Exponential v b c)
-> v (Exponential v a b) (Exponential v a b)
-> v (BinaryProduct v (Exponential v b c) (Exponential v a b))
     (Exponential v b 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 v (BinaryProduct v (Exponential v b c) (Exponential v a b))
  (Exponential v b c)
-> v (BinaryProduct v (Exponential v a b) a) b
-> v (BinaryProduct
        v
        (BinaryProduct v (Exponential v b c) (Exponential v a b))
        (BinaryProduct v (Exponential v a b) a))
     (BinaryProduct v (Exponential v b c) b)
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 -> v b b -> v (BinaryProduct v (Exponential v a b) a) b
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) v (BinaryProduct
     v
     (BinaryProduct v (Exponential v b c) (Exponential v a b))
     (BinaryProduct v (Exponential v a b) a))
  (BinaryProduct v (Exponential v b c) b)
-> 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))
-> v (BinaryProduct
        v (BinaryProduct v (Exponential v b c) (Exponential v a b)) a)
     (BinaryProduct v (Exponential v b c) 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 v c c -> v b b -> v (Exponential v b c) (Exponential v b 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 v b b -> v a a -> v (Exponential v a b) (Exponential v a 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 = Obj v (BinaryProduct v (Exponential v b c) (Exponential v a b))
-> v a a
-> v (BinaryProduct
        v (BinaryProduct v (Exponential v b c) (Exponential v a b)) a)
     (BinaryProduct v (Exponential v b c) (Exponential v a b))
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 b c) (Exponential v b c)
-> v (Exponential v a b) (Exponential v a b)
-> Obj v (BinaryProduct v (Exponential v b c) (Exponential v a b))
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 (BinaryProduct
     v (BinaryProduct v (Exponential v b c) (Exponential v a b)) a)
  (BinaryProduct v (Exponential v b c) (Exponential v a b))
-> v (BinaryProduct
        v (BinaryProduct v (Exponential v b c) (Exponential v a b)) a)
     (BinaryProduct v (Exponential v a b) a)
-> 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))
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)
&&& (v (Exponential v b c) (Exponential v b c)
-> v (Exponential v a b) (Exponential v a b)
-> v (BinaryProduct v (Exponential v b c) (Exponential v a b))
     (Exponential v a b)
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 v (BinaryProduct v (Exponential v b c) (Exponential v a b))
  (Exponential v a b)
-> v a a
-> v (BinaryProduct
        v (BinaryProduct v (Exponential v b c) (Exponential v a b)) a)
     (BinaryProduct v (Exponential v a b) 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)
*** v a a
a)

toSelf :: CartesianClosed v => v a b -> Arr (Self v) a b
toSelf :: v a b -> Arr (Self v) a b
toSelf v a b
v = Obj v (TerminalObject v)
-> Obj v a
-> Obj v b
-> v (BinaryProduct v (TerminalObject v) a) b
-> v (TerminalObject v) (Exponential v a b)
forall k1 (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, k1 ~ *) =>
Obj k2 x
-> Obj k2 y
-> Obj k2 z
-> k2 (BinaryProduct k2 x y) z
-> k2 x (Exponential k2 y z)
curry Obj v (TerminalObject v)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject (v a b -> Obj v a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src v a b
v) (v a b -> Obj v b
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 v a b
-> v (BinaryProduct v (TerminalObject v) a) a
-> v (BinaryProduct v (TerminalObject v) a) b
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj v (TerminalObject v)
-> Obj v a -> v (BinaryProduct v (TerminalObject v) a) a
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 (TerminalObject v)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject (v a b -> Obj v a
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 :: 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 = Obj v (TerminalObject v)
-> Obj v a
-> Obj v b
-> v (TerminalObject v) (Exponential v a b)
-> v (BinaryProduct v (TerminalObject v) a) b
forall k1 (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, k1 ~ *) =>
Obj k2 x
-> Obj k2 y
-> Obj k2 z
-> k2 x (Exponential k2 y z)
-> k2 (BinaryProduct k2 x y) z
uncurry Obj v (TerminalObject v)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject Obj v a
a Obj v b
b v (TerminalObject v) (Exponential v a b)
Arr (Self v) a b
arr v (BinaryProduct v (TerminalObject v) a) b
-> v a (BinaryProduct v (TerminalObject v) a) -> v a b
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Obj v a -> v a (TerminalObject v)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj v a
a v a (TerminalObject v)
-> Obj v a -> v a (BinaryProduct v (TerminalObject v) 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 :: 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) = Hom k
forall (k :: * -> * -> *). Hom k
Hom Hom k
-> Dom (Hom k) (a, b) (a, b)
-> Cod (Hom k) (Hom k :% (a, b)) (Hom k :% (a, b))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (k a a -> Op k a a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k a a
a Op k a a -> k b b -> (:**:) (Op k) k (a, b) (a, b)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: k b b
b)
  id :: Obj (InHask k) a -> Arr (InHask k) a a
id (InHask k a a
f) () = k a a
f -- meh
  comp :: 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 k b c -> k a b -> k a c
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


-- | 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 :: * -> * -> *
  -- | The codomain, or target category, of the functor.
  type ECod ftag :: * -> * -> *

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

  -- | @%%@ 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 :: * -> * -> *) = 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 %% :: 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
Obj (ECod (Id k)) (Id k :%% a)
a
  map :: 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 = Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod (Id k) $ (Id k :%% a, Id k :%% b))
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) %% :: (g :.: h)
-> Obj (EDom (g :.: h)) a -> Obj (ECod (g :.: h)) ((g :.: h) :%% a)
%% Obj (EDom (g :.: h)) a
a = g
g g -> Obj (EDom g) (h :%% a) -> Obj (ECod g) (g :%% (h :%% a))
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% (h
h h -> Obj (EDom h) a -> Obj (ECod h) (h :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom h) a
Obj (EDom (g :.: h)) a
a)
  map :: (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 = g
-> Obj (EDom g) (h :%% a)
-> Obj (EDom g) (h :%% b)
-> V (EDom g)
     (EDom g $ (h :%% a, h :%% b))
     (ECod g $ (g :%% (h :%% a), g :%% (h :%% 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 h -> Obj (EDom h) a -> Obj (ECod h) (h :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj k a
Obj (EDom h) a
a) (h
h h -> Obj (EDom h) b -> Obj (ECod h) (h :%% b)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj k b
Obj (EDom h) b
b) V (ECod g)
  (EDom g $ (h :%% a, h :%% b))
  (ECod g $ (g :%% (h :%% a), g :%% (h :%% b)))
-> V (ECod g) (EDom h $ (a, b)) (EDom g $ (h :%% a, h :%% b))
-> V (ECod g)
     (EDom h $ (a, b))
     (ECod g $ (g :%% (h :%% a), g :%% (h :%% b)))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. h
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod h $ (h :%% a, h :%% 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 h
h Obj k a
a Obj k b
b

data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) 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 %% :: 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
Obj (ECod (Const c1 c2 x)) (Const c1 c2 x :%% a)
x
  map :: 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 = Obj c2 x -> Arr c2 x x
forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id Obj c2 x
x V c2 (TerminalObject (V c2)) (c2 $ (x, x))
-> V c2 (c1 $ (a, b)) (TerminalObject (V c2))
-> V c2 (c1 $ (a, b)) (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
. Obj (V c2) (c1 $ (a, b))
-> V c2 (c1 $ (a, b)) (TerminalObject (V c2))
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate (Obj k a -> Obj k b -> Obj (V k) (k $ (a, 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)

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 %% :: Opposite f
-> Obj (EDom (Opposite f)) a
-> Obj (ECod (Opposite f)) (Opposite f :%% a)
%% EOp a = ECod f (f :%% a) (f :%% a) -> EOp (ECod f) (f :%% a) (f :%% a)
forall (k :: * -> * -> *) a b. k b a -> EOp k a b
EOp (f
f f -> Obj (EDom f) a -> ECod f (f :%% a) (f :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom f) a
a)
  map :: 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 a) (EOp b) = f
-> Obj (EDom f) b
-> Obj (EDom f) a
-> V (EDom f) (EDom f $ (b, a)) (ECod f $ (f :%% b, f :%% 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) b
b Obj (EDom f) 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) %% :: (f1 :<*>: f2)
-> Obj (EDom (f1 :<*>: f2)) a
-> Obj (ECod (f1 :<*>: f2)) ((f1 :<*>: f2) :%% a)
%% (a1 :<>: a2) = (f1
f1 f1 -> Obj (EDom f1) a1 -> ECod f1 (f1 :%% a1) (f1 :%% a1)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom f1) a1
a1) ECod f1 (f1 :%% a1) (f1 :%% a1)
-> Obj (ECod f2) (f2 :%% a2)
-> (:<>:)
     (ECod f1) (ECod f2) (f1 :%% a1, f2 :%% a2) (f1 :%% a1, f2 :%% a2)
forall (k1 :: * -> * -> *) (k2 :: * -> * -> *) a1 a2.
(V k1 ~ V k2) =>
Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
:<>: (f2
f2 f2 -> Obj (EDom f2) a2 -> Obj (ECod f2) (f2 :%% a2)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom f2) a2
a2)
  map :: (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) (a1 :<>: a2) (b1 :<>: b2) = f1
-> Obj (EDom f1) a1
-> Obj (EDom f1) a1
-> V (EDom f1)
     (EDom f1 $ (a1, a1))
     (ECod f1 $ (f1 :%% a1, f1 :%% a1))
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 V (ECod f2) (EDom f1 $ (a1, a1)) (ECod f1 $ (f1 :%% a1, f1 :%% a1))
-> V (ECod f2)
     (EDom f2 $ (a2, a2))
     (ECod f2 $ (f2 :%% a2, f2 :%% a2))
-> V (ECod f2)
     (BinaryProduct
        (V (ECod f2)) (EDom f1 $ (a1, a1)) (EDom f2 $ (a2, a2)))
     (BinaryProduct
        (V (ECod f2))
        (ECod f1 $ (f1 :%% a1, f1 :%% a1))
        (ECod f2 $ (f2 :%% a2, f2 :%% a2)))
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)
*** f2
-> Obj (EDom f2) a2
-> Obj (EDom f2) a2
-> V (EDom f2)
     (EDom f2 $ (a2, a2))
     (ECod f2 $ (f2 :%% a2, f2 :%% a2))
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 :: * -> * -> *) = 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 %% :: DiagProd k
-> Obj (EDom (DiagProd k)) a
-> Obj (ECod (DiagProd k)) (DiagProd k :%% a)
%% Obj (EDom (DiagProd k)) a
a = k a a
Obj (EDom (DiagProd k)) a
a k a a -> k a a -> (:<>:) k k (a, a) (a, a)
forall (k1 :: * -> * -> *) (k2 :: * -> * -> *) a1 a2.
(V k1 ~ V k2) =>
Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
:<>: k a a
Obj (EDom (DiagProd k)) a
a
  map :: 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 = Obj k a -> Obj k b -> Obj (V k) (k $ (a, 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 V k (k $ (a, b)) (k $ (a, b))
-> V k (k $ (a, b)) (k $ (a, b))
-> V k (k $ (a, b)) (BinaryProduct (V k) (k $ (a, b)) (k $ (a, 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)
&&& Obj k a -> Obj k b -> Obj (V k) (k $ (a, 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

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 % :: UnderlyingF f
-> Dom (UnderlyingF f) a b
-> Cod (UnderlyingF f) (UnderlyingF f :% a) (UnderlyingF f :% b)
% Underlying a ab b = Obj (ECod f) (f :%% a)
-> Arr (ECod f) (f :%% a) (f :%% b)
-> Obj (ECod f) (f :%% b)
-> Underlying (ECod f) (f :%% a) (f :%% b)
forall (k :: * -> * -> *) a b.
Obj k a -> Arr k a b -> Obj k b -> Underlying k a b
Underlying (f
f f -> Obj (EDom f) a -> Obj (ECod f) (f :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom f) a
a) (f
-> Obj (EDom f) a
-> Obj (EDom f) b
-> V (EDom f) (EDom f $ (a, b)) (ECod f $ (f :%% a, f :%% 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 Obj (EDom f) a
a Obj (EDom f) b
b V (ECod f) (EDom f $ (a, b)) (ECod f $ (f :%% a, f :%% b))
-> V (ECod f) (TerminalObject (V (ECod f))) (EDom f $ (a, b))
-> V (ECod f)
     (TerminalObject (V (ECod f)))
     (ECod f $ (f :%% a, f :%% 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
V (ECod f) (TerminalObject (V (ECod f))) (EDom f $ (a, b))
ab) (f
f f -> Obj (EDom f) b -> Obj (ECod f) (f :%% b)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom f) b
b)
  

data EHom (k :: * -> * -> *) = 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 %% :: EHom k
-> Obj (EDom (EHom k)) a -> Obj (ECod (EHom k)) (EHom k :%% a)
%% (EOp a :<>: b) = V k (k $ (a1, a2)) (k $ (a1, a2))
-> Self (V k) (k $ (a1, a2)) (k $ (a1, a2))
forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (Obj k a1 -> Obj k a2 -> V k (k $ (a1, a2)) (k $ (a1, a2))
forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k a1
a Obj k a2
b)
  map :: 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 a1 :<>: a2) (EOp b1 :<>: b2) = Obj (V k) (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
-> Obj (V k) (k $ (a1, a2))
-> Obj (V k) (k $ (a1, a2))
-> V k
     (BinaryProduct
        (V k)
        (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
        (k $ (a1, a2)))
     (k $ (a1, a2))
-> V k
     (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
     (Exponential (V k) (k $ (a1, a2)) (k $ (a1, a2)))
forall k1 (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, k1 ~ *) =>
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 Obj (V k) (k $ (a1, a1))
-> V k (k $ (a2, a2)) (k $ (a2, a2))
-> Obj (V k) (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
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 k (k $ (a2, a2)) (k $ (a2, a2))
ab) Obj (V k) (k $ (a1, a2))
a Obj (V k) (k $ (a1, a2))
b (Obj k a1
-> Obj k a1
-> Obj k a2
-> V k
     (BinaryProduct (V k) (k $ (a1, a2)) (k $ (a1, a1)))
     (k $ (a1, a2))
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 a1
b1 Obj k a1
a1 Obj k a2
b2 V k
  (BinaryProduct (V k) (k $ (a1, a2)) (k $ (a1, a1)))
  (k $ (a1, a2))
-> V k
     (BinaryProduct
        (V k)
        (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
        (k $ (a1, a2)))
     (BinaryProduct (V k) (k $ (a1, a2)) (k $ (a1, a1)))
-> V k
     (BinaryProduct
        (V k)
        (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
        (k $ (a1, a2)))
     (k $ (a1, a2))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Obj k a1
-> Obj k a2
-> Obj k a2
-> V k
     (BinaryProduct (V k) (k $ (a2, a2)) (k $ (a1, a2)))
     (k $ (a1, a2))
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 a1
a1 Obj k a2
a2 Obj k a2
b2 V k
  (BinaryProduct (V k) (k $ (a2, a2)) (k $ (a1, a2)))
  (k $ (a1, a2))
-> V k
     (BinaryProduct
        (V k)
        (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
        (k $ (a1, a2)))
     (BinaryProduct (V k) (k $ (a2, a2)) (k $ (a1, a2)))
-> V k
     (BinaryProduct
        (V k)
        (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
        (k $ (a1, a2)))
     (k $ (a1, a2))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (Obj (V k) (k $ (a1, a1))
-> V k (k $ (a2, a2)) (k $ (a2, a2))
-> V k
     (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
     (k $ (a2, a2))
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 V k (k $ (a2, a2)) (k $ (a2, a2))
ab V k
  (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
  (k $ (a2, a2))
-> Obj (V k) (k $ (a1, a2))
-> V k
     (BinaryProduct
        (V k)
        (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
        (k $ (a1, a2)))
     (BinaryProduct (V k) (k $ (a2, a2)) (k $ (a1, a2)))
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) V k
  (BinaryProduct
     (V k)
     (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
     (k $ (a1, a2)))
  (k $ (a1, a2))
-> V k
     (BinaryProduct
        (V k)
        (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
        (k $ (a1, a2)))
     (k $ (a1, a1))
-> V k
     (BinaryProduct
        (V k)
        (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
        (k $ (a1, a2)))
     (BinaryProduct (V k) (k $ (a1, a2)) (k $ (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)
&&& Obj (V k) (k $ (a1, a1))
-> V k (k $ (a2, a2)) (k $ (a2, a2))
-> V k
     (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
     (k $ (a1, a1))
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 V k (k $ (a2, a2)) (k $ (a2, a2))
ab V k
  (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
  (k $ (a1, a1))
-> V k
     (BinaryProduct
        (V k)
        (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
        (k $ (a1, a2)))
     (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
-> V k
     (BinaryProduct
        (V k)
        (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
        (k $ (a1, a2)))
     (k $ (a1, a1))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj (V k) (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
-> Obj (V k) (k $ (a1, a2))
-> V k
     (BinaryProduct
        (V k)
        (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
        (k $ (a1, a2)))
     (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
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 $ (a1, a1))
-> V k (k $ (a2, a2)) (k $ (a2, a2))
-> Obj (V k) (BinaryProduct (V k) (k $ (a1, a1)) (k $ (a2, a2)))
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 k (k $ (a2, a2)) (k $ (a2, a2))
ab) Obj (V k) (k $ (a1, a2))
a))
    where
      a :: Obj (V k) (k $ (a1, a2))
a = Obj k a1 -> Obj k a2 -> Obj (V k) (k $ (a1, a2))
forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k a1
a1 Obj k a2
a2
      b :: Obj (V k) (k $ (a1, a2))
b = Obj k a1 -> Obj k a2 -> Obj (V k) (k $ (a1, a2))
forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k a1
b1 Obj k a2
b2
      ba :: Obj (V k) (k $ (a1, a1))
ba = Obj k a1 -> Obj k a1 -> Obj (V k) (k $ (a1, a1))
forall (k :: * -> * -> *) a b.
ECategory k =>
Obj k a -> Obj k b -> Obj (V k) (k $ (a, b))
hom Obj k a1
b1 Obj k a1
a1
      ab :: V k (k $ (a2, a2)) (k $ (a2, a2))
ab = Obj k a2 -> Obj k a2 -> V k (k $ (a2, a2)) (k $ (a2, a2))
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


-- | Enriched natural transformations.
data ENat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * 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



-- | 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 %% :: 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 = V k (k $ (x, a)) (k $ (x, a))
-> Self (V k) (k $ (x, a)) (k $ (x, a))
forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (Obj k x -> Obj k a -> V k (k $ (x, a)) (k $ (x, 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 a
Obj (EDom (EHomX_ k x)) a
y)
  map :: 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 = Obj (V k) (k $ (a, b))
-> Obj (V k) (k $ (x, a))
-> Obj (V k) (k $ (x, b))
-> V k (BinaryProduct (V k) (k $ (a, b)) (k $ (x, a))) (k $ (x, b))
-> V k (k $ (a, b)) (Exponential (V k) (k $ (x, a)) (k $ (x, b)))
forall k1 (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, k1 ~ *) =>
Obj k2 x
-> Obj k2 y
-> Obj k2 z
-> k2 (BinaryProduct k2 x y) z
-> k2 x (Exponential k2 y z)
curry (Obj k a -> Obj k b -> Obj (V k) (k $ (a, 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) (Obj k x -> Obj k a -> Obj (V k) (k $ (x, 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 a
Obj k a
a) (Obj k x -> Obj k b -> Obj (V k) (k $ (x, 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 b
Obj k b
b) (Obj k x
-> Obj k a
-> Obj k b
-> V k (BinaryProduct (V k) (k $ (a, b)) (k $ (x, a))) (k $ (x, 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
Obj k a
a Obj k b
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 %% :: 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 = V k (k $ (a, x)) (k $ (a, x))
-> Self (V k) (k $ (a, x)) (k $ (a, x))
forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (Obj (EOp k) x -> Obj (EOp k) a -> Obj (V (EOp k)) (EOp k $ (x, 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 (EDom (EHom_X k x)) a
Obj (EOp k) a
y)
  map :: 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 = Obj (V k) (k $ (b, a))
-> Obj (V k) (k $ (a, x))
-> Obj (V k) (k $ (b, x))
-> V k (BinaryProduct (V k) (k $ (b, a)) (k $ (a, x))) (k $ (b, x))
-> V k (k $ (b, a)) (Exponential (V k) (k $ (a, x)) (k $ (b, x)))
forall k1 (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, k1 ~ *) =>
Obj k2 x
-> Obj k2 y
-> Obj k2 z
-> k2 (BinaryProduct k2 x y) z
-> k2 x (Exponential k2 y z)
curry (Obj k a -> Obj k b -> Obj (V k) (k $ (a, 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) (Obj (EOp k) x -> Obj (EOp k) a -> Obj (V (EOp k)) (EOp k $ (x, 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 a
Obj (EOp k) a
a) (Obj (EOp k) x -> Obj (EOp k) b -> Obj (V (EOp k)) (EOp k $ (x, 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 b
Obj (EOp k) b
b) (Obj (EOp k) x
-> Obj (EOp k) a
-> Obj (EOp k) b
-> V (EOp k)
     (BinaryProduct (V (EOp k)) (EOp k $ (a, b)) (EOp k $ (x, a)))
     (EOp k $ (x, 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
Obj (EOp k) a
a Obj k b
Obj (EOp k) b
b)



type VProfunctor k l t = EFunctorOf (EOp k :<>: l) (Self (V k)) t

type family End (v :: * -> * -> *) t :: *
class CartesianClosed v => HasEnds v where
  end :: (VProfunctor k k t, V k ~ v) => t -> Obj v (End v t)
  endCounit :: (VProfunctor k k t, V k ~ v) => t -> Obj k a -> v (End v t) (t :%% (a, a))
  endFactorizer :: (VProfunctor k k t, V k ~ v) => t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
  

newtype HaskEnd t = HaskEnd { HaskEnd t
-> forall (k :: * -> * -> *) a.
   VProfunctor k k t =>
   t -> Obj k a -> t :%% (a, a)
getHaskEnd :: forall k a. VProfunctor k k t => t -> Obj k a -> t :%% (a, a) }
type instance End (->) t = HaskEnd t
instance HasEnds (->) where
  end :: t -> Obj (->) (End (->) t)
end t
_ End (->) t
e = End (->) t
e
  endCounit :: t -> Obj k a -> End (->) t -> t :%% (a, a)
endCounit t
t Obj k a
a (HaskEnd e) = t -> Obj k a -> t :%% (a, a)
forall (k :: * -> * -> *) a.
VProfunctor k k t =>
t -> Obj k a -> t :%% (a, a)
e t
t Obj k a
a
  endFactorizer :: t -> (forall a. Obj k a -> x -> t :%% (a, a)) -> x -> End (->) t
endFactorizer t
_ forall a. Obj k a -> x -> t :%% (a, a)
e x
x = (forall (k :: * -> * -> *) a.
 VProfunctor k k t =>
 t -> Obj k a -> t :%% (a, a))
-> HaskEnd t
forall t.
(forall (k :: * -> * -> *) a.
 VProfunctor k k t =>
 t -> Obj k a -> t :%% (a, a))
-> HaskEnd t
HaskEnd (\t
_ Obj k a
a -> Obj k a -> x -> t :%% (a, a)
forall a. Obj k a -> x -> t :%% (a, a)
e Obj k a
Obj k a
a x
x)


data FunCat a b t s where
  FArr :: (EFunctorOf a b t, EFunctorOf a b s) => t -> s -> FunCat a b t s

type t :->>: s = EHom (ECod t) :.: (Opposite t :<*>: s)
(->>) :: (EFunctor t, EFunctor s, ECod t ~ ECod s, V (ECod t) ~ V (ECod s)) => t -> s -> t :->>: s
t
t ->> :: t -> s -> t :->>: s
->> s
s = EHom (ECod s)
forall (k :: * -> * -> *). EHom k
EHom EHom (ECod s)
-> (Opposite t :<*>: s) -> EHom (ECod s) :.: (Opposite t :<*>: s)
forall g h.
(EFunctor g, EFunctor h, ECod h ~ EDom g) =>
g -> h -> g :.: h
:.: (t -> Opposite t
forall f. EFunctor f => f -> Opposite f
Opposite t
t Opposite t -> s -> Opposite t :<*>: s
forall f1 f2. f1 -> f2 -> f1 :<*>: f2
:<*>: s
s)
-- | The enriched functor category @[a, b]@
instance (HasEnds (V a), V a ~ V b) => ECategory (FunCat a b) where
  type V (FunCat a b) = V a
  type FunCat a b $ (t, s) = End (V a) (t :->>: s)
  hom :: Obj (FunCat a b) a
-> Obj (FunCat a b) b -> Obj (V (FunCat a b)) (FunCat a b $ (a, b))
hom (FArr a
t a
_) (FArr b
s b
_) = (EHom b :.: (Opposite a :<*>: b))
-> Obj (V b) (End (V b) (EHom b :.: (Opposite a :<*>: b)))
forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end (a
t a -> b -> a :->>: b
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> b
s)
  id :: Obj (FunCat a b) a -> Arr (FunCat a b) a a
id (FArr a
t a
_) = (EHom b :.: (Opposite a :<*>: a))
-> (forall a.
    Obj a a
    -> V b
         (TerminalObject (V b))
         ((EHom b :.: (Opposite a :<*>: a)) :%% (a, a)))
-> V b
     (TerminalObject (V b))
     (End (V b) (EHom b :.: (Opposite a :<*>: a)))
forall (v :: * -> * -> *) (k :: * -> * -> *) t x.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
endFactorizer (a
t a -> a -> a :->>: a
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> a
t) (\Obj a a
a -> Obj b (a :%% a) -> Arr b (a :%% a) (a :%% a)
forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id (a
t a -> Obj (EDom a) a -> Obj (ECod a) (a :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj a a
Obj (EDom a) a
a))
  comp :: Obj (FunCat a b) a
-> Obj (FunCat a b) b
-> Obj (FunCat a b) c
-> V (FunCat a b)
     (BinaryProduct
        (V (FunCat a b)) (FunCat a b $ (b, c)) (FunCat a b $ (a, b)))
     (FunCat a b $ (a, c))
comp (FArr a
t a
_) (FArr b
s b
_) (FArr c
r c
_) = (EHom b :.: (Opposite a :<*>: c))
-> (forall a.
    Obj a a
    -> V b
         (BinaryProduct
            (V b)
            (End (V b) (EHom b :.: (Opposite b :<*>: c)))
            (End (V b) (EHom b :.: (Opposite a :<*>: b))))
         ((EHom b :.: (Opposite a :<*>: c)) :%% (a, a)))
-> V b
     (BinaryProduct
        (V b)
        (End (V b) (EHom b :.: (Opposite b :<*>: c)))
        (End (V b) (EHom b :.: (Opposite a :<*>: b))))
     (End (V b) (EHom b :.: (Opposite a :<*>: c)))
forall (v :: * -> * -> *) (k :: * -> * -> *) t x.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
endFactorizer (a
t a -> c -> a :->>: c
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> c
r) 
    (\Obj a a
a -> Obj b (a :%% a)
-> Obj b (b :%% a)
-> Obj b (c :%% a)
-> V b
     (BinaryProduct
        (V b) (b $ (b :%% a, c :%% a)) (b $ (a :%% a, b :%% a)))
     (b $ (a :%% a, c :%% a))
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 (a
t a -> Obj (EDom a) a -> Obj (ECod a) (a :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj a a
Obj (EDom a) a
a) (b
s b -> Obj (EDom b) a -> Obj (ECod b) (b :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj a a
Obj (EDom b) a
a) (c
r c -> Obj (EDom c) a -> Obj (ECod c) (c :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj a a
Obj (EDom c) a
a) V b
  (BinaryProduct
     (V b) (b $ (b :%% a, c :%% a)) (b $ (a :%% a, b :%% a)))
  (b $ (a :%% a, c :%% a))
-> V b
     (BinaryProduct
        (V b)
        (End (V b) (EHom b :.: (Opposite b :<*>: c)))
        (End (V b) (EHom b :.: (Opposite a :<*>: b))))
     (BinaryProduct
        (V b) (b $ (b :%% a, c :%% a)) (b $ (a :%% a, b :%% a)))
-> V b
     (BinaryProduct
        (V b)
        (End (V b) (EHom b :.: (Opposite b :<*>: c)))
        (End (V b) (EHom b :.: (Opposite a :<*>: b))))
     (b $ (a :%% a, c :%% a))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. ((EHom b :.: (Opposite b :<*>: c))
-> Obj a a
-> V b
     (End (V b) (EHom b :.: (Opposite b :<*>: c)))
     ((EHom b :.: (Opposite b :<*>: c)) :%% (a, a))
forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj k a -> v (End v t) (t :%% (a, a))
endCounit (b
s b -> c -> b :->>: c
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> c
r) Obj a a
a V b
  (End (V b) (EHom b :.: (Opposite b :<*>: c)))
  (b $ (b :%% a, c :%% a))
-> V b
     (End (V b) (EHom b :.: (Opposite a :<*>: b)))
     (b $ (a :%% a, b :%% a))
-> V b
     (BinaryProduct
        (V b)
        (End (V b) (EHom b :.: (Opposite b :<*>: c)))
        (End (V b) (EHom b :.: (Opposite a :<*>: b))))
     (BinaryProduct
        (V b) (b $ (b :%% a, c :%% a)) (b $ (a :%% a, b :%% 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)
*** (EHom b :.: (Opposite a :<*>: b))
-> Obj a a
-> V b
     (End (V b) (EHom b :.: (Opposite a :<*>: b)))
     ((EHom b :.: (Opposite a :<*>: b)) :%% (a, a))
forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj k a -> v (End v t) (t :%% (a, a))
endCounit (a
t a -> b -> a :->>: b
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> b
s) Obj a a
a))


data EndFunctor (k :: * -> * -> *) = EndFunctor
instance (HasEnds (V k), ECategory k) => EFunctor (EndFunctor k) where
  type EDom (EndFunctor k) = FunCat (EOp k :<>: k) (Self (V k))
  type ECod (EndFunctor k) = Self (V k)
  type EndFunctor k :%% t = End (V k) t
  EndFunctor k
EndFunctor %% :: EndFunctor k
-> Obj (EDom (EndFunctor k)) a
-> Obj (ECod (EndFunctor k)) (EndFunctor k :%% a)
%% (FArr t _) = V k (End (V k) a) (End (V k) a)
-> Self (V k) (End (V k) a) (End (V k) a)
forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self (a -> V k (End (V k) a) (End (V k) a)
forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end a
t)
  map :: EndFunctor k
-> Obj k a
-> Obj k b
-> V k
     (k $ (a, b))
     (ECod (EndFunctor k) $ (EndFunctor k :%% a, EndFunctor k :%% b))
map EndFunctor k
EndFunctor (FArr f _) (FArr g _) = Obj (V k) (End (V k) (EHom (Self (V k)) :.: (Opposite a :<*>: b)))
-> Obj (V k) (End (V k) a)
-> Obj (V k) (End (V k) b)
-> V k
     (BinaryProduct
        (V k)
        (End (V k) (EHom (Self (V k)) :.: (Opposite a :<*>: b)))
        (End (V k) a))
     (End (V k) b)
-> V k
     (End (V k) (EHom (Self (V k)) :.: (Opposite a :<*>: b)))
     (Exponential (V k) (End (V k) a) (End (V k) b))
forall k1 (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, k1 ~ *) =>
Obj k2 x
-> Obj k2 y
-> Obj k2 z
-> k2 (BinaryProduct k2 x y) z
-> k2 x (Exponential k2 y z)
curry ((EHom (Self (V k)) :.: (Opposite a :<*>: b))
-> Obj
     (V k) (End (V k) (EHom (Self (V k)) :.: (Opposite a :<*>: b)))
forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end (a
f a -> b -> a :->>: b
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> b
g)) (a -> Obj (V k) (End (V k) a)
forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end a
f) (b -> Obj (V k) (End (V k) b)
forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end b
g) (b
-> (forall a.
    Obj k a
    -> V k
         (BinaryProduct
            (V k)
            (End (V k) (EHom (Self (V k)) :.: (Opposite a :<*>: b)))
            (End (V k) a))
         (b :%% (a, a)))
-> V k
     (BinaryProduct
        (V k)
        (End (V k) (EHom (Self (V k)) :.: (Opposite a :<*>: b)))
        (End (V k) a))
     (End (V k) b)
forall (v :: * -> * -> *) (k :: * -> * -> *) t x.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
endFactorizer b
g (\Obj k a
a -> 
    let aa :: (:<>:) (EOp k) k (a, a) (a, a)
aa = Obj k a -> EOp k a a
forall (k :: * -> * -> *) a b. k b a -> EOp k a b
EOp Obj k a
a EOp k a a -> Obj k a -> (:<>:) (EOp k) k (a, a) (a, a)
forall (k1 :: * -> * -> *) (k2 :: * -> * -> *) a1 a2.
(V k1 ~ V k2) =>
Obj k1 a1 -> Obj k2 a2 -> (:<>:) k1 k2 (a1, a2) (a1, a2)
:<>: Obj k a
a in Obj (V k) (a :%% (a, a))
-> Obj (V k) (b :%% (a, a))
-> V k
     (BinaryProduct
        (V k)
        (Exponential (V k) (a :%% (a, a)) (b :%% (a, a)))
        (a :%% (a, a)))
     (b :%% (a, a))
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 (Self (V k) (a :%% (a, a)) (a :%% (a, a))
-> Obj (V k) (a :%% (a, a))
forall (v :: * -> * -> *) a b. Self v a b -> v a b
getSelf (a
f a -> Obj (EDom a) (a, a) -> Obj (ECod a) (a :%% (a, a))
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom a) (a, a)
(:<>:) (EOp k) k (a, a) (a, a)
aa)) (Self (V k) (b :%% (a, a)) (b :%% (a, a))
-> Obj (V k) (b :%% (a, a))
forall (v :: * -> * -> *) a b. Self v a b -> v a b
getSelf (b
g b -> Obj (EDom b) (a, a) -> Obj (ECod b) (b :%% (a, a))
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj (EDom b) (a, a)
(:<>:) (EOp k) k (a, a) (a, a)
aa)) V k
  (BinaryProduct
     (V k)
     (Exponential (V k) (a :%% (a, a)) (b :%% (a, a)))
     (a :%% (a, a)))
  (b :%% (a, a))
-> V k
     (BinaryProduct
        (V k)
        (End (V k) (EHom (Self (V k)) :.: (Opposite a :<*>: b)))
        (End (V k) a))
     (BinaryProduct
        (V k)
        (Exponential (V k) (a :%% (a, a)) (b :%% (a, a)))
        (a :%% (a, a)))
-> V k
     (BinaryProduct
        (V k)
        (End (V k) (EHom (Self (V k)) :.: (Opposite a :<*>: b)))
        (End (V k) a))
     (b :%% (a, a))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. ((EHom (Self (V k)) :.: (Opposite a :<*>: b))
-> (:<>:) (EOp k) k (a, a) (a, a)
-> V k
     (End (V k) (EHom (Self (V k)) :.: (Opposite a :<*>: b)))
     ((EHom (Self (V k)) :.: (Opposite a :<*>: b)) :%% ((a, a), (a, a)))
forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj k a -> v (End v t) (t :%% (a, a))
endCounit (a
f a -> b -> a :->>: b
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> b
g) (:<>:) (EOp k) k (a, a) (a, a)
aa V k
  (End (V k) (EHom (Self (V k)) :.: (Opposite a :<*>: b)))
  (Exponential (V k) (a :%% (a, a)) (b :%% (a, a)))
-> V k (End (V k) a) (a :%% (a, a))
-> V k
     (BinaryProduct
        (V k)
        (End (V k) (EHom (Self (V k)) :.: (Opposite a :<*>: b)))
        (End (V k) a))
     (BinaryProduct
        (V k)
        (Exponential (V k) (a :%% (a, a)) (b :%% (a, a)))
        (a :%% (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)
*** a -> Obj k a -> V k (End (V k) a) (a :%% (a, a))
forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj k a -> v (End v t) (t :%% (a, a))
endCounit a
f Obj k a
a)))
    

-- d :: j -> k, w :: j -> Self (V k)
type family WeigtedLimit (k :: * -> * -> *) w d :: *
type Lim w d = WeigtedLimit (ECod d) w d

class HasEnds (V k) => HasLimits k where
  limitObj :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k (Lim w d)
  limit    :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHomX_ k e :.: d))) (k $ (e, Lim w d))
  limitInv :: (EFunctorOf j k d, EFunctorOf j (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (e, Lim w d)) (End (V k) (w :->>: (EHomX_ k e :.: d)))

-- d :: j -> k, w :: EOp j -> Self (V k)
type family WeigtedColimit (k :: * -> * -> *) w d :: *
type Colim w d = WeigtedColimit (ECod d) w d

class HasEnds (V k) => HasColimits k where
  colimitObj :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k (Colim w d)
  colimit    :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (End (V k) (w :->>: (EHom_X k e :.: Opposite d))) (k $ (Colim w d, e))
  colimitInv :: (EFunctorOf j k d, EFunctorOf (EOp j) (Self (V k)) w) => w -> d -> Obj k e -> V k (k $ (Colim w d, e)) (End (V k) (w :->>: (EHom_X k e :.: Opposite d)))
  

type instance WeigtedLimit (Self v) w d = End v (w :->>: d)
instance HasEnds v => HasLimits (Self v) where
  limitObj :: w -> d -> Obj (Self v) (Lim w d)
limitObj w
w d
d = v (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
  (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
-> Self
     v
     (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
     (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self ((EHom (Self v) :.: (Opposite w :<*>: d))
-> v (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
     (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end (w
w w -> d -> w :->>: d
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> d
d))
  limit :: w
-> d
-> Obj (Self v) e
-> V (Self v)
     (End (V (Self v)) (w :->>: (EHomX_ (Self v) e :.: d)))
     (Self v $ (e, Lim w d))
limit w
w d
d (Self v e e
e) = let wed :: w :->>: (EHomX_ (Self v) e :.: d)
wed = w
w w -> (EHomX_ (Self v) e :.: d) -> w :->>: (EHomX_ (Self v) e :.: d)
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> (Obj (Self v) e -> EHomX_ (Self v) e
forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ (v e e -> Obj (Self v) e
forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self v e e
e) EHomX_ (Self v) e -> d -> EHomX_ (Self v) e :.: d
forall g h.
(EFunctor g, EFunctor h, ECod h ~ EDom g) =>
g -> h -> g :.: h
:.: d
d) in Obj
  v
  (End
     v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
-> v e e
-> Obj v (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
-> v (BinaryProduct
        v
        (End
           v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
        e)
     (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
-> v (End
        v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
     (Exponential v e (End v (EHom (Self v) :.: (Opposite w :<*>: d))))
forall k1 (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, k1 ~ *) =>
Obj k2 x
-> Obj k2 y
-> Obj k2 z
-> k2 (BinaryProduct k2 x y) z
-> k2 x (Exponential k2 y z)
curry ((EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d)))
-> Obj
     v
     (End
        v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end w :->>: (EHomX_ (Self v) e :.: d)
EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))
wed) v e e
e ((EHom (Self v) :.: (Opposite w :<*>: d))
-> Obj v (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end (w
w w -> d -> w :->>: d
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> d
d)) 
    ((EHom (Self v) :.: (Opposite w :<*>: d))
-> (forall a.
    Obj j a
    -> v (BinaryProduct
            v
            (End
               v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
            e)
         ((EHom (Self v) :.: (Opposite w :<*>: d)) :%% (a, a)))
-> v (BinaryProduct
        v
        (End
           v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
        e)
     (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
forall (v :: * -> * -> *) (k :: * -> * -> *) t x.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
endFactorizer (w
w w -> d -> w :->>: d
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> d
d) (\Obj j a
a -> let { Self v (w :%% a) (w :%% a)
wa = w
w w -> Obj (EDom w) a -> Obj (ECod w) (w :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj j a
Obj (EDom w) a
a; Self v (d :%% a) (d :%% a)
da = d
d d -> Obj (EDom d) a -> Obj (ECod d) (d :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj j a
Obj (EDom d) a
a } in v e e
-> Obj v (Exponential v (w :%% a) (d :%% a))
-> v (BinaryProduct
        v (Exponential v e (Exponential v (w :%% a) (d :%% a))) e)
     (Exponential v (w :%% a) (d :%% a))
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 e e
e (v (d :%% a) (d :%% a)
da v (d :%% a) (d :%% a)
-> v (w :%% a) (w :%% a)
-> Obj v (Exponential v (w :%% a) (d :%% a))
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 (w :%% a) (w :%% a)
wa) v (BinaryProduct
     v (Exponential v e (Exponential v (w :%% a) (d :%% a))) e)
  (Exponential v (w :%% a) (d :%% a))
-> v (BinaryProduct
        v
        (End
           v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
        e)
     (BinaryProduct
        v (Exponential v e (Exponential v (w :%% a) (d :%% a))) e)
-> v (BinaryProduct
        v
        (End
           v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
        e)
     (Exponential v (w :%% a) (d :%% a))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (v (w :%% a) (w :%% a)
-> v e e
-> v (d :%% a) (d :%% a)
-> v (Exponential v (w :%% a) (Exponential v e (d :%% a)))
     (Exponential v e (Exponential v (w :%% a) (d :%% a)))
forall k1 (k2 :: k1 -> k1 -> *) (a :: k1) (b :: k1) (c :: k1).
CartesianClosed k2 =>
Obj k2 a
-> Obj k2 b
-> Obj k2 c
-> k2
     (Exponential k2 a (Exponential k2 b c))
     (Exponential k2 b (Exponential k2 a c))
flip v (w :%% a) (w :%% a)
wa v e e
e v (d :%% a) (d :%% a)
da v (Exponential v (w :%% a) (Exponential v e (d :%% a)))
  (Exponential v e (Exponential v (w :%% a) (d :%% a)))
-> v (End
        v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
     (Exponential v (w :%% a) (Exponential v e (d :%% a)))
-> v (End
        v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
     (Exponential v e (Exponential v (w :%% a) (d :%% a)))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d)))
-> Obj j a
-> v (End
        v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
     ((EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d)))
      :%% (a, a))
forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj k a -> v (End v t) (t :%% (a, a))
endCounit w :->>: (EHomX_ (Self v) e :.: d)
EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))
wed Obj j a
a v (End
     v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
  (Exponential v e (Exponential v (w :%% a) (d :%% a)))
-> v e e
-> v (BinaryProduct
        v
        (End
           v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
        e)
     (BinaryProduct
        v (Exponential v e (Exponential v (w :%% a) (d :%% a))) e)
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 e e
e)))
  limitInv :: w
-> d
-> Obj (Self v) e
-> V (Self v)
     (Self v $ (e, Lim w d))
     (End (V (Self v)) (w :->>: (EHomX_ (Self v) e :.: d)))
limitInv w
w d
d (Self v e e
e) = let wed :: w :->>: (EHomX_ (Self v) e :.: d)
wed = w
w w -> (EHomX_ (Self v) e :.: d) -> w :->>: (EHomX_ (Self v) e :.: d)
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> (Obj (Self v) e -> EHomX_ (Self v) e
forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ (v e e -> Obj (Self v) e
forall (v :: * -> * -> *) a b. v a b -> Self v a b
Self v e e
e) EHomX_ (Self v) e -> d -> EHomX_ (Self v) e :.: d
forall g h.
(EFunctor g, EFunctor h, ECod h ~ EDom g) =>
g -> h -> g :.: h
:.: d
d) in (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d)))
-> (forall a.
    Obj j a
    -> v (Exponential
            v e (End v (EHom (Self v) :.: (Opposite w :<*>: d))))
         ((EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d)))
          :%% (a, a)))
-> v (Exponential
        v e (End v (EHom (Self v) :.: (Opposite w :<*>: d))))
     (End
        v (EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))))
forall (v :: * -> * -> *) (k :: * -> * -> *) t x.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
endFactorizer w :->>: (EHomX_ (Self v) e :.: d)
EHom (Self v) :.: (Opposite w :<*>: (EHomX_ (Self v) e :.: d))
wed 
    (\Obj j a
a -> let { Self v (w :%% a) (w :%% a)
wa = w
w w -> Obj (EDom w) a -> Obj (ECod w) (w :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj j a
Obj (EDom w) a
a; Self v (d :%% a) (d :%% a)
da = d
d d -> Obj (EDom d) a -> Obj (ECod d) (d :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj j a
Obj (EDom d) a
a } in v e e
-> v (w :%% a) (w :%% a)
-> v (d :%% a) (d :%% a)
-> v (Exponential v e (Exponential v (w :%% a) (d :%% a)))
     (Exponential v (w :%% a) (Exponential v e (d :%% a)))
forall k1 (k2 :: k1 -> k1 -> *) (a :: k1) (b :: k1) (c :: k1).
CartesianClosed k2 =>
Obj k2 a
-> Obj k2 b
-> Obj k2 c
-> k2
     (Exponential k2 a (Exponential k2 b c))
     (Exponential k2 b (Exponential k2 a c))
flip v e e
e v (w :%% a) (w :%% a)
wa v (d :%% a) (d :%% a)
da v (Exponential v e (Exponential v (w :%% a) (d :%% a)))
  (Exponential v (w :%% a) (Exponential v e (d :%% a)))
-> v (Exponential
        v e (End v (EHom (Self v) :.: (Opposite w :<*>: d))))
     (Exponential v e (Exponential v (w :%% a) (d :%% a)))
-> v (Exponential
        v e (End v (EHom (Self v) :.: (Opposite w :<*>: d))))
     (Exponential v (w :%% a) (Exponential v e (d :%% a)))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. ((EHom (Self v) :.: (Opposite w :<*>: d))
-> Obj j a
-> v (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
     ((EHom (Self v) :.: (Opposite w :<*>: d)) :%% (a, a))
forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj k a -> v (End v t) (t :%% (a, a))
endCounit (w
w w -> d -> w :->>: d
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> d
d) Obj j a
a v (End v (EHom (Self v) :.: (Opposite w :<*>: d)))
  (Exponential v (w :%% a) (d :%% a))
-> v e e
-> v (Exponential
        v e (End v (EHom (Self v) :.: (Opposite w :<*>: d))))
     (Exponential v e (Exponential v (w :%% a) (d :%% a)))
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 e e
e))



yoneda    :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (End (V k) (EHomX_ k x :->>: f)) (f :%% x)
yoneda :: f -> Obj k x -> V k (End (V k) (EHomX_ k x :->>: f)) (f :%% x)
yoneda f
f Obj k x
x = Obj (V k) (k $ (x, x))
-> Obj (V k) (f :%% x)
-> V k
     (BinaryProduct
        (V k) (Exponential (V k) (k $ (x, x)) (f :%% x)) (k $ (x, x)))
     (f :%% x)
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 (Obj k x -> Obj k x -> Obj (V k) (k $ (x, x))
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 x
x) (Self (V k) (f :%% x) (f :%% x) -> Obj (V k) (f :%% x)
forall (v :: * -> * -> *) a b. Self v a b -> v a b
getSelf (f
f f -> Obj (EDom f) x -> Obj (ECod f) (f :%% x)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj k x
Obj (EDom f) x
x)) V k
  (BinaryProduct
     (V k) (Exponential (V k) (k $ (x, x)) (f :%% x)) (k $ (x, x)))
  (f :%% x)
-> V k
     (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
     (BinaryProduct
        (V k) (Exponential (V k) (k $ (x, x)) (f :%% x)) (k $ (x, x)))
-> V k
     (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
     (f :%% x)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. ((EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f))
-> Obj k x
-> V k
     (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
     ((EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f))
      :%% (x, x))
forall (v :: * -> * -> *) (k :: * -> * -> *) t a.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj k a -> v (End v t) (t :%% (a, a))
endCounit (Obj k x -> EHomX_ k x
forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ Obj k x
x EHomX_ k x -> f -> EHomX_ k x :->>: f
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> f
f) Obj k x
x V k
  (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
  (Exponential (V k) (k $ (x, x)) (f :%% x))
-> V k
     (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
     (k $ (x, x))
-> V k
     (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
     (BinaryProduct
        (V k) (Exponential (V k) (k $ (x, x)) (f :%% x)) (k $ (x, x)))
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 k x -> Arr k x x
forall (k :: * -> * -> *) a. ECategory k => Obj k a -> Arr k a a
id Obj k x
x V k (TerminalObject (V k)) (k $ (x, x))
-> V k
     (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
     (TerminalObject (V k))
-> V k
     (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
     (k $ (x, x))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj
  (V k)
  (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
-> V k
     (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
     (TerminalObject (V k))
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate ((EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f))
-> Obj
     (V k)
     (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
forall (v :: * -> * -> *) (k :: * -> * -> *) t.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> Obj v (End v t)
end (Obj k x -> EHomX_ k x
forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ Obj k x
x EHomX_ k x -> f -> EHomX_ k x :->>: f
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> f
f)))

yonedaInv :: forall f k x. (HasEnds (V k), EFunctorOf k (Self (V k)) f) => f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))
yonedaInv :: f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))
yonedaInv f
f Obj k x
x = (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f))
-> (forall a.
    Obj k a
    -> V k
         (f :%% x)
         ((EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f))
          :%% (a, a)))
-> V k
     (f :%% x)
     (End (V k) (EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f)))
forall (v :: * -> * -> *) (k :: * -> * -> *) t x.
(HasEnds v, VProfunctor k k t, V k ~ v) =>
t -> (forall a. Obj k a -> v x (t :%% (a, a))) -> v x (End v t)
endFactorizer (Obj k x -> EHomX_ k x
forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ Obj k x
x EHomX_ k x -> f -> EHomX_ k x :->>: f
forall t s.
(EFunctor t, EFunctor s, ECod t ~ ECod s,
 V (ECod t) ~ V (ECod s)) =>
t -> s -> t :->>: s
->> f
f) forall a.
Obj k a -> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))
forall a.
Obj k a
-> V k
     (f :%% x)
     ((EHom (Self (V k)) :.: (Opposite (EHomX_ k x) :<*>: f))
      :%% (a, a))
h
  where
    h :: Obj k a -> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))
    h :: Obj k a -> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))
h Obj k a
a = Obj (V k) (f :%% x)
-> Obj (V k) (k $ (x, a))
-> Obj (V k) (f :%% a)
-> V k (BinaryProduct (V k) (f :%% x) (k $ (x, a))) (f :%% a)
-> V k (f :%% x) (Exponential (V k) (k $ (x, a)) (f :%% a))
forall k1 (k2 :: k1 -> k1 -> *) (x :: k1) (y :: k1) (z :: k1).
(CartesianClosed k2, k1 ~ *) =>
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) (f :%% x)
fx Obj (V k) (k $ (x, a))
xa Obj (V k) (f :%% a)
fa (Obj (V k) (f :%% x)
-> Obj (V k) (f :%% a)
-> V k
     (BinaryProduct
        (V k) (Exponential (V k) (f :%% x) (f :%% a)) (f :%% x))
     (f :%% a)
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 Obj (V k) (f :%% x)
fx Obj (V k) (f :%% a)
fa V k
  (BinaryProduct
     (V k) (Exponential (V k) (f :%% x) (f :%% a)) (f :%% x))
  (f :%% a)
-> V k
     (BinaryProduct (V k) (f :%% x) (k $ (x, a)))
     (BinaryProduct
        (V k) (Exponential (V k) (f :%% x) (f :%% a)) (f :%% x))
-> V k (BinaryProduct (V k) (f :%% x) (k $ (x, a))) (f :%% a)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. (f
-> Obj k x
-> Obj k a
-> V k (k $ (x, a)) (ECod f $ (f :%% x, f :%% 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 k x
x Obj k a
a V k (k $ (x, a)) (Exponential (V k) (f :%% x) (f :%% a))
-> V k (BinaryProduct (V k) (f :%% x) (k $ (x, a))) (k $ (x, a))
-> V k
     (BinaryProduct (V k) (f :%% x) (k $ (x, a)))
     (Exponential (V k) (f :%% x) (f :%% a))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj (V k) (f :%% x)
-> Obj (V k) (k $ (x, a))
-> V k (BinaryProduct (V k) (f :%% x) (k $ (x, a))) (k $ (x, a))
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) (f :%% x)
fx Obj (V k) (k $ (x, a))
xa V k
  (BinaryProduct (V k) (f :%% x) (k $ (x, a)))
  (Exponential (V k) (f :%% x) (f :%% a))
-> V k (BinaryProduct (V k) (f :%% x) (k $ (x, a))) (f :%% x)
-> V k
     (BinaryProduct (V k) (f :%% x) (k $ (x, a)))
     (BinaryProduct
        (V k) (Exponential (V k) (f :%% x) (f :%% a)) (f :%% x))
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 k) (f :%% x)
-> Obj (V k) (k $ (x, a))
-> V k (BinaryProduct (V k) (f :%% x) (k $ (x, a))) (f :%% x)
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) (f :%% x)
fx Obj (V k) (k $ (x, a))
xa))
      where
        xa :: Obj (V k) (k $ (x, a))
xa = Obj k x -> Obj k a -> Obj (V k) (k $ (x, 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 a
a
        Self Obj (V k) (f :%% x)
fx = f
f f -> Obj (EDom f) x -> Obj (ECod f) (f :%% x)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj k x
Obj (EDom f) x
x
        Self Obj (V k) (f :%% a)
fa = f
f f -> Obj (EDom f) a -> Obj (ECod f) (f :%% a)
forall ftag a.
EFunctor ftag =>
ftag -> Obj (EDom ftag) a -> Obj (ECod ftag) (ftag :%% a)
%% Obj k a
Obj (EDom f) a
a

data Y (k :: * -> * -> *) = Y
-- | Yoneda embedding
instance (ECategory k, HasEnds (V k)) => EFunctor (Y k) where
  type EDom (Y k) = EOp k
  type ECod (Y k) = FunCat k (Self (V k))
  type Y k :%% x = EHomX_ k x
  Y k
Y %% :: Y k -> Obj (EDom (Y k)) a -> Obj (ECod (Y k)) (Y k :%% a)
%% EOp x = EHomX_ k a
-> EHomX_ k a -> FunCat k (Self (V k)) (EHomX_ k a) (EHomX_ k a)
forall (a :: * -> * -> *) (b :: * -> * -> *) t s.
(EFunctorOf a b t, EFunctorOf a b s) =>
t -> s -> FunCat a b t s
FArr (Obj k a -> EHomX_ k a
forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ Obj k a
x) (Obj k a -> EHomX_ k a
forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ Obj k a
x)
  map :: Y k
-> Obj k a
-> Obj k b
-> V k (k $ (a, b)) (ECod (Y k) $ (Y k :%% a, Y k :%% b))
map Y k
Y (EOp a) (EOp b) = EHomX_ k b
-> Obj k a
-> V k (EHomX_ k b :%% a) (End (V k) (EHomX_ k a :->>: EHomX_ k b))
forall f (k :: * -> * -> *) x.
(HasEnds (V k), EFunctorOf k (Self (V k)) f) =>
f -> Obj k x -> V k (f :%% x) (End (V k) (EHomX_ k x :->>: f))
yonedaInv (Obj k b -> EHomX_ k b
forall (k :: * -> * -> *) x. Obj k x -> EHomX_ k x
EHomX_ Obj k b
b) Obj k a
a


data One
data Two
data Three
data PosetTest a b where
  One :: PosetTest One One
  Two :: PosetTest Two Two
  Three :: PosetTest Three Three

type family Poset3 a b where
  Poset3 Two One = Fls
  Poset3 Three One = Fls
  Poset3 Three Two = Fls
  Poset3 a b = Tru
instance ECategory PosetTest where
  type V PosetTest = Boolean
  type PosetTest $ (a, b) = Poset3 a b
  hom :: Obj PosetTest a
-> Obj PosetTest b -> Obj (V PosetTest) (PosetTest $ (a, b))
hom Obj PosetTest a
One Obj PosetTest b
One = Boolean Tru Tru
Obj (V PosetTest) (PosetTest $ (a, b))
Tru
  hom Obj PosetTest a
One Obj PosetTest b
Two = Boolean Tru Tru
Obj (V PosetTest) (PosetTest $ (a, b))
Tru
  hom Obj PosetTest a
One Obj PosetTest b
Three = Boolean Tru Tru
Obj (V PosetTest) (PosetTest $ (a, b))
Tru
  hom Obj PosetTest a
Two Obj PosetTest b
One = Boolean Fls Fls
Obj (V PosetTest) (PosetTest $ (a, b))
Fls
  hom Obj PosetTest a
Two Obj PosetTest b
Two = Boolean Tru Tru
Obj (V PosetTest) (PosetTest $ (a, b))
Tru
  hom Obj PosetTest a
Two Obj PosetTest b
Three = Boolean Tru Tru
Obj (V PosetTest) (PosetTest $ (a, b))
Tru
  hom Obj PosetTest a
Three Obj PosetTest b
One = Boolean Fls Fls
Obj (V PosetTest) (PosetTest $ (a, b))
Fls
  hom Obj PosetTest a
Three Obj PosetTest b
Two = Boolean Fls Fls
Obj (V PosetTest) (PosetTest $ (a, b))
Fls
  hom Obj PosetTest a
Three Obj PosetTest b
Three = Boolean Tru Tru
Obj (V PosetTest) (PosetTest $ (a, b))
Tru

  id :: Obj PosetTest a -> Arr PosetTest a a
id Obj PosetTest a
One = Arr PosetTest a a
Boolean Tru Tru
Tru
  id Obj PosetTest a
Two = Arr PosetTest a a
Boolean Tru Tru
Tru
  id Obj PosetTest a
Three = Arr PosetTest a a
Boolean Tru Tru
Tru
  comp :: Obj PosetTest a
-> Obj PosetTest b
-> Obj PosetTest c
-> V PosetTest
     (BinaryProduct
        (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
     (PosetTest $ (a, c))
comp Obj PosetTest a
One Obj PosetTest b
One Obj PosetTest c
One = Boolean Tru Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Tru
  comp Obj PosetTest a
One Obj PosetTest b
One Obj PosetTest c
Two = Boolean Tru Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Tru
  comp Obj PosetTest a
One Obj PosetTest b
One Obj PosetTest c
Three = Boolean Tru Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Tru
  comp Obj PosetTest a
One Obj PosetTest b
Two Obj PosetTest c
One = Boolean Fls Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
F2T
  comp Obj PosetTest a
One Obj PosetTest b
Two Obj PosetTest c
Two = Boolean Tru Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Tru
  comp Obj PosetTest a
One Obj PosetTest b
Two Obj PosetTest c
Three = Boolean Tru Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Tru
  comp Obj PosetTest a
One Obj PosetTest b
Three Obj PosetTest c
One = Boolean Fls Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
F2T
  comp Obj PosetTest a
One Obj PosetTest b
Three Obj PosetTest c
Two = Boolean Fls Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
F2T
  comp Obj PosetTest a
One Obj PosetTest b
Three Obj PosetTest c
Three = Boolean Tru Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Tru
  comp Obj PosetTest a
Two Obj PosetTest b
One Obj PosetTest c
One = Boolean Fls Fls
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Fls
  comp Obj PosetTest a
Two Obj PosetTest b
One Obj PosetTest c
Two = Boolean Fls Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
F2T
  comp Obj PosetTest a
Two Obj PosetTest b
One Obj PosetTest c
Three = Boolean Fls Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
F2T
  comp Obj PosetTest a
Two Obj PosetTest b
Two Obj PosetTest c
One = Boolean Fls Fls
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Fls
  comp Obj PosetTest a
Two Obj PosetTest b
Two Obj PosetTest c
Two = Boolean Tru Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Tru
  comp Obj PosetTest a
Two Obj PosetTest b
Two Obj PosetTest c
Three = Boolean Tru Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Tru
  comp Obj PosetTest a
Two Obj PosetTest b
Three Obj PosetTest c
One = Boolean Fls Fls
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Fls
  comp Obj PosetTest a
Two Obj PosetTest b
Three Obj PosetTest c
Two = Boolean Fls Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
F2T
  comp Obj PosetTest a
Two Obj PosetTest b
Three Obj PosetTest c
Three = Boolean Tru Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Tru
  comp Obj PosetTest a
Three Obj PosetTest b
One Obj PosetTest c
One = Boolean Fls Fls
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Fls
  comp Obj PosetTest a
Three Obj PosetTest b
One Obj PosetTest c
Two = Boolean Fls Fls
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Fls
  comp Obj PosetTest a
Three Obj PosetTest b
One Obj PosetTest c
Three = Boolean Fls Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
F2T
  comp Obj PosetTest a
Three Obj PosetTest b
Two Obj PosetTest c
One = Boolean Fls Fls
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Fls
  comp Obj PosetTest a
Three Obj PosetTest b
Two Obj PosetTest c
Two = Boolean Fls Fls
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Fls
  comp Obj PosetTest a
Three Obj PosetTest b
Two Obj PosetTest c
Three = Boolean Fls Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
F2T
  comp Obj PosetTest a
Three Obj PosetTest b
Three Obj PosetTest c
One = Boolean Fls Fls
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Fls
  comp Obj PosetTest a
Three Obj PosetTest b
Three Obj PosetTest c
Two = Boolean Fls Fls
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Fls
  comp Obj PosetTest a
Three Obj PosetTest b
Three Obj PosetTest c
Three = Boolean Tru Tru
V PosetTest
  (BinaryProduct
     (V PosetTest) (PosetTest $ (b, c)) (PosetTest $ (a, b)))
  (PosetTest $ (a, c))
Tru