{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LinearTypes #-}

module Control.Category.Constrained where

import Prelude hiding ((.),id)
import Data.Kind
import Data.Constraint
import Data.Type.Equality


type O2 k a b = (Obj k a, Obj k b)
type O3 k a b c =
  (Obj k a, Obj k b, Obj k c)
type O4 k a b c d =
  (Obj k a, Obj k b, Obj k c, Obj k d)

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where
  All c '[] = ()
  All c (x ': xs) = (c x, All c xs)
  

class Trivial a
instance Trivial a

instance ProdObj Trivial where
  prodobj :: forall a b. (Trivial a, Trivial b) => Dict (Trivial (a ⊗ b))
prodobj = forall (a :: Constraint). a => Dict a
Dict
  objprod :: forall z a b.
(z ~ (a ⊗ b), Trivial z) =>
Dict (Trivial a, Trivial b)
objprod = forall (a :: Constraint). a => Dict a
Dict
  objunit :: Dict (Trivial ())
objunit = forall (a :: Constraint). a => Dict a
Dict


class Category k where
  type Obj k :: Type -> Constraint {-<-}
  type Obj k = Trivial {->-}
  id   :: Obj k a => a `k` a
  (∘)  ::   (Obj k a, Obj k b, Obj k c) =>
             (b `k` c) -> (a `k` b) -> a `k` c

infixl 8 .
infixl 8 ∘

(.) :: (Category k, O3 k a b c) => k b c -> k a b -> k a c
. :: forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
(.) = forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
(∘)

class ProdObj con where
  prodobj :: (con a, con b) => Dict (con (a⊗b))
  objprod :: forall z a b. (z ~ (a⊗b), con z) => Dict (con a, con b)
  objunit :: Dict (con ())

objProd :: forall k a b z. (z ~ (a⊗b), Obj k z, Monoidal k) => Dict (Obj k a, Obj k b)
objProd :: forall (k :: * -> * -> *) a b z.
(z ~ (a ⊗ b), Obj k z, Monoidal k) =>
Dict (Obj k a, Obj k b)
objProd = forall (con :: * -> Constraint) z a b.
(ProdObj con, z ~ (a ⊗ b), con z) =>
Dict (con a, con b)
objprod

prodObj ::  forall k a b. (Monoidal k, Obj k a, Obj k b) => Dict (Obj k (a⊗b))
prodObj :: forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj = forall (con :: * -> Constraint) a b.
(ProdObj con, con a, con b) =>
Dict (con (a ⊗ b))
prodobj

unitObj ::  forall k. (Monoidal k) => Dict (Obj k ())
unitObj :: forall (k :: * -> * -> *). Monoidal k => Dict (Obj k ())
unitObj = forall (con :: * -> Constraint). ProdObj con => Dict (con ())
objunit


infixr 0 //
(//) :: Dict c -> (c => k) -> k
Dict c
Dict // :: forall (c :: Constraint) k. Dict c -> (c => k) -> k
// c => k
k = c => k
k

type a ⊗ b = (a,b)
infixr 7 ⊗


class ({-<-}ProdObj (Obj k),{->-}Category k) => Monoidal k where
  (×)      :: {-<-}(Obj k a, Obj k b, Obj k c, Obj k d) =>{->-} (a `k` b) -> (c `k` d) -> (a ⊗ c) `k` (b ⊗ d)
  swap     :: {-<-}(Obj k a, Obj k b) =>{->-} (a ⊗ b) `k` (b ⊗ a)
  assoc    :: {-<-}(Obj k a, Obj k b, Obj k c) =>{->-} ((a ⊗ b) ⊗ c) `k` (a ⊗ (b ⊗ c))
  assoc'   :: {-<-}(Obj k a, Obj k b, Obj k c) =>{->-} (a ⊗ (b ⊗ c)) `k` ((a ⊗ b) ⊗ c)
  unitor   :: {-<-}(Obj k a) =>{->-} a `k` (a ⊗ ())
  unitor'  :: {-<-}(Obj k a) =>{->-} (a ⊗ ()) `k` a

class Monoidal k => Cartesian k where
  exl   ::  {-<-} forall a b. O2 k a b                     => {->-}   (a ⊗ b) `k` a
  exr   ::  {-<-} forall a b. O2 k a b                     => {->-}   (a ⊗ b) `k` b
  dis   ::  {-<-} forall a.   Obj k a                      => {->-}   a `k` ()
  dup   ::  {-<-} (Obj k a, Obj k (a⊗a))                   => {->-}   a `k` (a ⊗ a)
  (▵)   ::  {-<-} forall a b c. (Obj k a,Obj k b, Obj k c) => {->-}   (a `k` b) -> (a `k` c) -> a `k` (b ⊗ c)

  {-<-}
  {-# MINIMAL exl,exr,dup | exl,exr,(▵) | dis,dup | dis,(▵) #-}
  dis = forall (k :: * -> * -> *) a. (Cartesian k, Obj k a) => k a ()
disDefault
  dup = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c.
(Cartesian k, Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (b ⊗ c)
▵ forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
  exl = forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exlDefault
  exr = forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exrDefault
  (▵) = forall (k :: * -> * -> *) a b c.
(Cartesian k, O3 k a b c) =>
k a b -> k a c -> k a (b ⊗ c)
(▵!)
  {->-}

disDefault :: forall k a. (Cartesian k, Obj k a) =>  a `k` ()
disDefault :: forall (k :: * -> * -> *) a. (Cartesian k, Obj k a) => k a ()
disDefault = forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k a (a ⊗ ())
unitor
     forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @a @()
     forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *). Monoidal k => Dict (Obj k ())
unitObj @k

exlDefault :: forall k a b. (Cartesian k, O2 k a b) =>  (a ⊗ b) `k` a
exlDefault :: forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exlDefault = forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Cartesian k, Obj k a) => k a ()
dis)
          forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @a @b
          forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @a @()
          forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *). Monoidal k => Dict (Obj k ())
unitObj @k

exrDefault :: forall k a b. (Cartesian k, O2 k a b) =>  (a ⊗ b) `k` b
exrDefault :: forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exrDefault = forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap forall (k :: * -> * -> *) a b c.
(Category k, Obj k a, Obj k b, Obj k c) =>
k b c -> k a b -> k a c
∘ (forall (k :: * -> * -> *) a. (Cartesian k, Obj k a) => k a ()
dis forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id)
          forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @a @b
          forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @b @()
          forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @() @b
          forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *). Monoidal k => Dict (Obj k ())
unitObj @k

(▵!) :: forall k a b c. (Cartesian k, O3 k a b c) =>   (a `k` b) -> (a `k` c) -> a `k` (b ⊗ c)
k a b
f ▵! :: forall (k :: * -> * -> *) a b c.
(Cartesian k, O3 k a b c) =>
k a b -> k a c -> k a (b ⊗ c)
▵! k a c
g = (k a b
f forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× k a c
g) forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a.
(Cartesian k, Obj k a, Obj k (a ⊗ a)) =>
k a (a ⊗ a)
dup
          forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @a @a
          forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @b @c

cartesianCross :: (Obj k (b1 ⊗ b2), Obj k b3, Obj k c, Obj k b1,
                     Obj k b2, Cartesian k) =>
                    k b1 b3 -> k b2 c -> k (b1 ⊗ b2) (b3 ⊗ c)
cartesianCross :: forall (k :: * -> * -> *) b1 b2 b3 c.
(Obj k (b1 ⊗ b2), Obj k b3, Obj k c, Obj k b1, Obj k b2,
 Cartesian k) =>
k b1 b3 -> k b2 c -> k (b1 ⊗ b2) (b3 ⊗ c)
cartesianCross k b1 b3
a k b2 c
b = (k b1 b3
a forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl) forall (k :: * -> * -> *) a b c.
(Cartesian k, Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (b ⊗ c)
▵ (k b2 c
b forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr)
cartesianUnitor :: forall a k. (Obj k a, Obj k (), Cartesian k) => a `k` (a ⊗ ())
cartesianUnitor :: forall a (k :: * -> * -> *).
(Obj k a, Obj k (), Cartesian k) =>
k a (a ⊗ ())
cartesianUnitor = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c.
(Cartesian k, Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (b ⊗ c)
▵ forall (k :: * -> * -> *) a. (Cartesian k, Obj k a) => k a ()
dis

cartesianUnitor' :: forall a k. (Obj k a, Obj k (), Cartesian k) => (a ⊗ ()) `k` a
cartesianUnitor' :: forall a (k :: * -> * -> *).
(Obj k a, Obj k (), Cartesian k) =>
k (a ⊗ ()) a
cartesianUnitor' = forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl

cartesianSwap :: forall a b k. (Obj k a, Obj k b, Cartesian k) => (a ⊗ b) `k` (b ⊗ a)
cartesianSwap :: forall a b (k :: * -> * -> *).
(Obj k a, Obj k b, Cartesian k) =>
k (a ⊗ b) (b ⊗ a)
cartesianSwap = forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr forall (k :: * -> * -> *) a b c.
(Cartesian k, Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (b ⊗ c)
▵ forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl
     forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @a @b

cartesianAssoc :: forall a b c k. (Obj k a, Obj k b, Obj k c, Cartesian k) => ((a ⊗ b) ⊗ c) `k` (a ⊗ (b ⊗ c))
cartesianAssoc :: forall a b c (k :: * -> * -> *).
(Obj k a, Obj k b, Obj k c, Cartesian k) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
cartesianAssoc = (forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl) forall (k :: * -> * -> *) a b c.
(Cartesian k, Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (b ⊗ c)
▵ ((forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl) forall (k :: * -> * -> *) a b c.
(Cartesian k, Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (b ⊗ c)
▵ forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr)
     forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @(a,b) @c
     forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @a @b
     forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @b @c

cartesianAssoc' :: forall a b c k. (Obj k a, Obj k b, Obj k c, Cartesian k) => (a ⊗ (b ⊗ c)) `k` ((a ⊗ b) ⊗ c)
cartesianAssoc' :: forall a b c (k :: * -> * -> *).
(Obj k a, Obj k b, Obj k c, Cartesian k) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
cartesianAssoc' = (forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl forall (k :: * -> * -> *) a b c.
(Cartesian k, Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (b ⊗ c)
▵ (forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr)) forall (k :: * -> * -> *) a b c.
(Cartesian k, Obj k a, Obj k b, Obj k c) =>
k a b -> k a c -> k a (b ⊗ c)
▵ (forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr)
     forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @a @(b,c)
     forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @a @b
     forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @b @c



class Monoidal k => CoCartesian k where
  inl   :: {-<-} O2 k a b                                 => {->-} a `k` (a ⊗ b)
  inr   :: {-<-} O2 k a b                                 => {->-} b `k` (a ⊗ b)
  new   :: {-<-} forall a. (Obj k a)                      => {->-} () `k` a
  jam   :: {-<-} Obj k a                                  => {->-} (a⊗a) `k` a
  (▿)   :: {-<-} forall a b c. (Obj k a,Obj k b, Obj k c) => {->-} (b `k` a) -> (c `k` a) -> (b ⊗ c) `k` a

  {-<-}
  jam = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c.
(CoCartesian k, Obj k a, Obj k b, Obj k c) =>
k b a -> k c a -> k (b ⊗ c) a
▿ forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
  new = forall (k :: * -> * -> *) a. (Obj k a, CoCartesian k) => k () a
newDefault
  (▿) = forall (k :: * -> * -> *) a b c.
(O3 k a b c, CoCartesian k) =>
k b a -> k c a -> k (b ⊗ c) a
(▿!)
  {->-}

jamDefault :: (Obj k a, CoCartesian k) => (a⊗a) `k` a
jamDefault :: forall (k :: * -> * -> *) a.
(Obj k a, CoCartesian k) =>
k (a ⊗ a) a
jamDefault = forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c.
(CoCartesian k, Obj k a, Obj k b, Obj k c) =>
k b a -> k c a -> k (b ⊗ c) a
▿ forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id

newDefault :: forall k a. (Obj k a, CoCartesian k) => () `k` a
newDefault :: forall (k :: * -> * -> *) a. (Obj k a, CoCartesian k) => k () a
newDefault = forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b.
(CoCartesian k, O2 k a b) =>
k b (a ⊗ b)
inr
        forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @a @()
        forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *). Monoidal k => Dict (Obj k ())
unitObj @k

(▿!) ::  forall k a b c. (O3 k a b c, CoCartesian k) => (b `k` a) -> (c `k` a) -> (b ⊗ c) `k` a
k b a
f ▿! :: forall (k :: * -> * -> *) a b c.
(O3 k a b c, CoCartesian k) =>
k b a -> k c a -> k (b ⊗ c) a
▿! k c a
g = forall (k :: * -> * -> *) a.
(CoCartesian k, Obj k a) =>
k (a ⊗ a) a
jam forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. (k b a
f forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× k c a
g)
            forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @a @a
            forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
Dict (Obj k (a ⊗ b))
prodObj @k @b @c

transp :: forall a b c d k con . (con ~ Obj k, Monoidal k, O4 k a b c d, (forall α β. (con α, con β) => con (α,β)))
       => ((a,b) ⊗ (c,d)) `k` ((a,c) ⊗ (b,d))
transp :: forall a b c d (k :: * -> * -> *) (con :: * -> Constraint).
(con ~ Obj k, Monoidal k, O4 k a b c d,
 forall α β. (con α, con β) => con (α, β)) =>
k ((a, b) ⊗ (c, d)) ((a, c) ⊗ (b, d))
transp = forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc' forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. (forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× (forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. (forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap forall (k :: * -> * -> *) a b c d.
(Monoidal k, Obj k a, Obj k b, Obj k c, Obj k d) =>
k a b -> k c d -> k (a ⊗ c) (b ⊗ d)
× forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
assoc')) forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. forall (k :: * -> * -> *) a b c.
(Monoidal k, Obj k a, Obj k b, Obj k c) =>
k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
assoc

-- -- Poor man's infix arrows.
-- -- http://haskell.1045720.n5.nabble.com/Type-operators-in-GHC-td5154978i20.html
-- type a - (c :: * -> * -> *) = c a
-- type c > b                  = c b

-- infix 2 -
-- infix 1 >


class Cartesian k => Closed k where
  -- expObj' :: forall a b. SObj k a -> SObj k b -> SObj k (a -> b)
  apply :: O2 k a b => ((a -> b) ⊗ a) `k`  b
  curry :: O3 k a b c => ((a ⊗ b) `k` c) -> (a `k` (b -> c))


class Invertible k where
  dual :: (a `k` b) -> b `k` a

type Hopf k = (Cartesian k, CoCartesian k)
  -- (laws unstated as usual...)
  -- jam . dup = id
  -- etc.

instance Category (FUN x) where
  id :: forall a. Obj (FUN x) a => a %x -> a
id a
x = a
x
  b %x -> c
f ∘ :: forall a b c.
(Obj (FUN x) a, Obj (FUN x) b, Obj (FUN x) c) =>
(b %x -> c) -> (a %x -> b) -> a %x -> c
∘ a %x -> b
g = \a
x -> b %x -> c
f (a %x -> b
g a
x)

instance Monoidal (FUN m) where
  (a %m -> b
f × :: forall a b c d.
(Obj (FUN m) a, Obj (FUN m) b, Obj (FUN m) c, Obj (FUN m) d) =>
(a %m -> b) -> (c %m -> d) -> (a ⊗ c) %m -> b ⊗ d
× c %m -> d
g) (a
a,c
b) = (a %m -> b
f a
a, c %m -> d
g c
b)
  assoc :: forall a b c.
(Obj (FUN m) a, Obj (FUN m) b, Obj (FUN m) c) =>
((a ⊗ b) ⊗ c) %m -> a ⊗ (b ⊗ c)
assoc ((a
x,b
y),c
z) = (a
x,(b
y,c
z)) 
  assoc' :: forall a b c.
(Obj (FUN m) a, Obj (FUN m) b, Obj (FUN m) c) =>
(a ⊗ (b ⊗ c)) %m -> (a ⊗ b) ⊗ c
assoc' (a
x,(b
y,c
z)) = ((a
x,b
y),c
z)  
  swap :: forall a b. (Obj (FUN m) a, Obj (FUN m) b) => (a ⊗ b) %m -> b ⊗ a
swap (a
x,b
y) = (b
y,a
x)
  unitor :: forall a. Obj (FUN m) a => a %m -> a ⊗ ()
unitor = (,())
  unitor' :: forall a. Obj (FUN m) a => (a ⊗ ()) %m -> a
unitor' (a
x,()) = a
x

instance Cartesian (->) where
  exl :: forall a b. O2 (->) a b => (a ⊗ b) -> a
exl = forall a b. (a, b) -> a
fst
  exr :: forall a b. O2 (->) a b => (a ⊗ b) -> b
exr = forall a b. (a, b) -> b
snd
  (a -> b
f ▵ :: forall a b c.
(Obj (->) a, Obj (->) b, Obj (->) c) =>
(a -> b) -> (a -> c) -> a -> (b ⊗ c)
▵ a -> c
g) a
x = (a -> b
f a
x, a -> c
g a
x)
  dup :: forall a. (Obj (->) a, Obj (->) (a ⊗ a)) => a -> (a ⊗ a)
dup a
x = (a
x,a
x)

instance Closed (->) where
  apply :: forall a b. O2 (->) a b => ((a -> b) ⊗ a) -> b
apply (a -> b
f,a
x) = a -> b
f a
x
  curry :: forall a b c. O3 (->) a b c => ((a ⊗ b) -> c) -> a -> (b -> c)
curry = forall a b c. ((a, b) -> c) -> a -> b -> c
Prelude.curry

type Comparator k = forall a b b'. k a b -> k a b' -> Maybe (b :~: b')

class Category k => HasCompare k where
  compareMorphs :: Comparator k

-- | Equality-witnessing order type
data Order a b where
  LT, GT :: Order a b
  EQ :: Order a a