{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RecursiveDo #-}
{-# 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 = Dict (Trivial (a ⊗ b))
forall (a :: Constraint). a => Dict a
Dict
  objprod :: forall z a b.
(z ~ (a ⊗ b), Trivial z) =>
Dict (Trivial a, Trivial b)
objprod = Dict (Trivial a, Trivial b)
forall (a :: Constraint). a => Dict a
Dict
  objunit :: Dict (Trivial ())
objunit = Dict (Trivial ())
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
(.) = 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 = Dict (Obj k a, Obj k b)
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 = Dict (Obj k (a, b))
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 = Dict (Obj k ())
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 = 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 = k a ()
forall (k :: * -> * -> *) a. (Cartesian k, Obj k a) => k a ()
disDefault
  dup = k a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id k a a -> k a a -> k a (a ⊗ a)
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 a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
  exl = k (a ⊗ b) a
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exlDefault
  exr = k (a ⊗ b) b
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exrDefault
  (▵) = k a b -> k a c -> k a (b ⊗ c)
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 = k (a ⊗ ()) ()
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr k (a ⊗ ()) () -> k a (a ⊗ ()) -> k a ()
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k a (a ⊗ ())
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k a (a ⊗ ())
unitor
     (Obj k (a ⊗ ()) => k a ()) -> Dict (Obj k (a ⊗ ())) -> k 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 @a @()
     (Obj k () => k a ()) -> Dict (Obj k ()) -> 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 = k (a ⊗ ()) a
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' k (a ⊗ ()) a -> k (a ⊗ b) (a ⊗ ()) -> k (a ⊗ b) a
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. (k a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id k a a -> k b () -> k (a ⊗ b) (a ⊗ ())
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 b ()
forall (k :: * -> * -> *) a. (Cartesian k, Obj k a) => k a ()
dis)
          (Obj k (a ⊗ b) => k (a ⊗ b) a)
-> Dict (Obj k (a ⊗ b)) -> k (a ⊗ b) 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 @a @b
          (Obj k (a ⊗ ()) => k (a ⊗ b) a)
-> Dict (Obj k (a ⊗ ())) -> k (a ⊗ b) 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 @a @()
          (Obj k () => k (a ⊗ b) a) -> Dict (Obj k ()) -> k (a ⊗ b) 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 = k (b ⊗ ()) b
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' k (b ⊗ ()) b -> k (() ⊗ b) (b ⊗ ()) -> k (() ⊗ b) b
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
∘ k (() ⊗ b) (b ⊗ ())
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap k (() ⊗ b) b -> k (a ⊗ b) (() ⊗ b) -> k (a ⊗ b) b
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
∘ (k a ()
forall (k :: * -> * -> *) a. (Cartesian k, Obj k a) => k a ()
dis k a () -> k b b -> k (a ⊗ b) (() ⊗ b)
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 b b
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id)
          (Obj k (a ⊗ b) => k (a ⊗ b) b)
-> Dict (Obj k (a ⊗ b)) -> k (a ⊗ b) 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 @b
          (Obj k (b ⊗ ()) => k (a ⊗ b) b)
-> Dict (Obj k (b ⊗ ())) -> k (a ⊗ b) 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 @()
          (Obj k (() ⊗ b) => k (a ⊗ b) b)
-> Dict (Obj k (() ⊗ b)) -> k (a ⊗ b) 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
          (Obj k () => k (a ⊗ b) b) -> Dict (Obj k ()) -> k (a ⊗ b) 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 k a b -> k a c -> k (a ⊗ a) (b ⊗ c)
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) k (a ⊗ a) (b ⊗ c) -> k a (a ⊗ a) -> k a (b ⊗ c)
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k a (a ⊗ a)
forall (k :: * -> * -> *) a.
(Cartesian k, Obj k a, Obj k (a ⊗ a)) =>
k a (a ⊗ a)
dup
          (Obj k (a ⊗ a) => k a (b ⊗ c))
-> Dict (Obj k (a ⊗ a)) -> 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 @a
          (Obj k (b ⊗ c) => k a (b ⊗ c))
-> Dict (Obj k (b ⊗ c)) -> 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 @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 k b1 b3 -> k (b1 ⊗ b2) b1 -> k (b1 ⊗ b2) b3
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k (b1 ⊗ b2) b1
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl) k (b1 ⊗ b2) b3 -> k (b1 ⊗ b2) c -> k (b1 ⊗ b2) (b3 ⊗ c)
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 k b2 c -> k (b1 ⊗ b2) b2 -> k (b1 ⊗ b2) c
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k (b1 ⊗ b2) b2
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 = k a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id k a a -> k a () -> k a (a ⊗ ())
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 a ()
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' = k (a ⊗ ()) a
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 = k (a ⊗ b) b
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr k (a ⊗ b) b -> k (a ⊗ b) a -> k (a ⊗ b) (b ⊗ a)
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 (a ⊗ b) a
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl
     (Obj k (a ⊗ b) => k (a ⊗ b) (b ⊗ a))
-> Dict (Obj k (a ⊗ b)) -> k (a ⊗ b) (b ⊗ 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 @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 = (k (a ⊗ b) a
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl k (a ⊗ b) a -> k ((a ⊗ b) ⊗ c) (a ⊗ b) -> k ((a ⊗ b) ⊗ c) a
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k ((a ⊗ b) ⊗ c) (a ⊗ b)
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl) k ((a ⊗ b) ⊗ c) a
-> k ((a ⊗ b) ⊗ c) (b ⊗ c) -> k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c))
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 (a ⊗ b) b
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr k (a ⊗ b) b -> k ((a ⊗ b) ⊗ c) (a ⊗ b) -> k ((a ⊗ b) ⊗ c) b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k ((a ⊗ b) ⊗ c) (a ⊗ b)
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl) k ((a ⊗ b) ⊗ c) b -> k ((a ⊗ b) ⊗ c) c -> k ((a ⊗ b) ⊗ c) (b ⊗ c)
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 ((a ⊗ b) ⊗ c) c
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr)
     (Obj k ((a ⊗ b) ⊗ c) => k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c)))
-> Dict (Obj k ((a ⊗ b) ⊗ c)) -> k ((a ⊗ b) ⊗ c) (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) @c
     (Obj k (a ⊗ b) => k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c)))
-> Dict (Obj k (a ⊗ b)) -> k ((a ⊗ b) ⊗ c) (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
     (Obj k (b ⊗ c) => k ((a ⊗ b) ⊗ c) (a ⊗ (b ⊗ c)))
-> Dict (Obj k (b ⊗ c)) -> k ((a ⊗ b) ⊗ c) (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 @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' = (k (a ⊗ (b ⊗ c)) a
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl k (a ⊗ (b ⊗ c)) a -> k (a ⊗ (b ⊗ c)) b -> k (a ⊗ (b ⊗ c)) (a ⊗ b)
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 (b ⊗ c) b
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) a
exl k (b ⊗ c) b -> k (a ⊗ (b ⊗ c)) (b ⊗ c) -> k (a ⊗ (b ⊗ c)) b
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k (a ⊗ (b ⊗ c)) (b ⊗ c)
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr)) k (a ⊗ (b ⊗ c)) (a ⊗ b)
-> k (a ⊗ (b ⊗ c)) c -> k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c)
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 (b ⊗ c) c
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr k (b ⊗ c) c -> k (a ⊗ (b ⊗ c)) (b ⊗ c) -> k (a ⊗ (b ⊗ c)) c
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k (a ⊗ (b ⊗ c)) (b ⊗ c)
forall (k :: * -> * -> *) a b.
(Cartesian k, O2 k a b) =>
k (a ⊗ b) b
exr)
     (Obj k (a ⊗ (b ⊗ c)) => k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c))
-> Dict (Obj k (a ⊗ (b ⊗ c))) -> k (a ⊗ (b ⊗ c)) ((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,c)
     (Obj k (a ⊗ b) => k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c))
-> Dict (Obj k (a ⊗ b)) -> k (a ⊗ (b ⊗ c)) ((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
     (Obj k (b ⊗ c) => k (a ⊗ (b ⊗ c)) ((a ⊗ b) ⊗ c))
-> Dict (Obj k (b ⊗ c)) -> k (a ⊗ (b ⊗ c)) ((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 @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 = k a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id k a a -> k a a -> k (a ⊗ a) a
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
▿ k a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id
  new = k () a
forall (k :: * -> * -> *) a. (Obj k a, CoCartesian k) => k () a
newDefault
  (▿) = k b a -> k c a -> k (b ⊗ c) a
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 = k a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id k a a -> k a a -> k (a ⊗ a) a
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
▿ k a 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 = k (a ⊗ ()) a
forall (k :: * -> * -> *) a. (Monoidal k, Obj k a) => k (a ⊗ ()) a
unitor' k (a ⊗ ()) a -> k () (a ⊗ ()) -> k () a
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k () (a ⊗ ())
forall (k :: * -> * -> *) a b.
(CoCartesian k, O2 k a b) =>
k b (a ⊗ b)
inr
        (Obj k (a ⊗ ()) => k () a) -> Dict (Obj k (a ⊗ ())) -> k () 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 @a @()
        (Obj k () => k () a) -> Dict (Obj k ()) -> 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 = k (a ⊗ a) a
forall (k :: * -> * -> *) a.
(CoCartesian k, Obj k a) =>
k (a ⊗ a) a
jam k (a ⊗ a) a -> k (b ⊗ c) (a ⊗ a) -> k (b ⊗ c) a
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 k b a -> k c a -> k (b ⊗ c) (a ⊗ a)
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)
            (Obj k (a ⊗ a) => k (b ⊗ c) a)
-> Dict (Obj k (a ⊗ a)) -> k (b ⊗ c) 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 @a @a
            (Obj k (b ⊗ c) => k (b ⊗ c) a)
-> Dict (Obj k (b ⊗ c)) -> k (b ⊗ c) 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 = k (a ⊗ (c ⊗ (b ⊗ d))) ((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' k (a ⊗ (c ⊗ (b ⊗ d))) ((a ⊗ c) ⊗ (b ⊗ d))
-> k (a ⊗ (b ⊗ (c ⊗ d))) (a ⊗ (c ⊗ (b ⊗ d)))
-> k (a ⊗ (b ⊗ (c ⊗ d))) ((a ⊗ c) ⊗ (b ⊗ d))
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. (k a a
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id k a a
-> k (b ⊗ (c ⊗ d)) (c ⊗ (b ⊗ d))
-> k (a ⊗ (b ⊗ (c ⊗ d))) (a ⊗ (c ⊗ (b ⊗ d)))
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 ⊗ b) ⊗ d) (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 k ((c ⊗ b) ⊗ d) (c ⊗ (b ⊗ d))
-> k ((b ⊗ c) ⊗ d) ((c ⊗ b) ⊗ d) -> k ((b ⊗ c) ⊗ d) (c ⊗ (b ⊗ d))
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. (k (b ⊗ c) (c ⊗ b)
forall (k :: * -> * -> *) a b.
(Monoidal k, Obj k a, Obj k b) =>
k (a ⊗ b) (b ⊗ a)
swap k (b ⊗ c) (c ⊗ b) -> k d d -> k ((b ⊗ c) ⊗ d) ((c ⊗ b) ⊗ d)
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 d d
forall (k :: * -> * -> *) a. (Category k, Obj k a) => k a a
id) k ((b ⊗ c) ⊗ d) (c ⊗ (b ⊗ d))
-> k (b ⊗ (c ⊗ d)) ((b ⊗ c) ⊗ d) -> k (b ⊗ (c ⊗ d)) (c ⊗ (b ⊗ d))
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k (b ⊗ (c ⊗ d)) ((b ⊗ c) ⊗ 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')) k (a ⊗ (b ⊗ (c ⊗ d))) ((a ⊗ c) ⊗ (b ⊗ d))
-> k ((a ⊗ b) ⊗ (c ⊗ d)) (a ⊗ (b ⊗ (c ⊗ d)))
-> k ((a ⊗ b) ⊗ (c ⊗ d)) ((a ⊗ c) ⊗ (b ⊗ d))
forall (k :: * -> * -> *) a b c.
(Category k, O3 k a b c) =>
k b c -> k a b -> k a c
. k ((a ⊗ b) ⊗ (c ⊗ d)) (a ⊗ (b ⊗ (c ⊗ 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

-- -- 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 = (a, b) -> a
forall a b. (a, b) -> a
fst
  exr :: forall a b. O2 (->) a b => (a ⊗ b) -> b
exr = (a, b) -> b
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 = ((a, b) -> c) -> a -> b -> c
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