{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Proarrow.Category.Monoidal where

import Data.Kind (Constraint)
import Prelude (($))

import Proarrow.Core (CAT, PRO, Promonad(..), CategoryOf(..), Profunctor (..), dimapDefault, obj, Obj)

class (CategoryOf k, Ob (Unit :: k)) => Monoidal k where
  type Unit :: k
  type (a :: k) ** (b :: k) :: k
  par :: ((a :: k) ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
  leftUnitor :: Obj (a :: k) -> Unit ** a ~> a
  leftUnitorInv :: Obj (a :: k) -> a ~> Unit ** a
  rightUnitor :: Obj (a :: k) -> a ** Unit ~> a
  rightUnitorInv :: Obj (a :: k) -> a ~> a ** Unit
  associator :: Obj (a :: k) -> Obj b -> Obj c -> (a ** b) ** c ~> a ** (b ** c)
  associatorInv :: Obj (a :: k) -> Obj b -> Obj c -> a ** (b ** c) ~> (a ** b) ** c

class Monoidal k => SymMonoidal k where
  swap' :: Obj (a :: k) -> Obj b -> (a ** b) ~> (b ** a)

swap :: forall {k} a b. (SymMonoidal k, Ob (a :: k), Ob b) => (a ** b) ~> (b ** a)
swap :: forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = Obj a -> Obj b -> (a ** b) ~> (b ** a)
forall (a :: k) (b :: k). Obj a -> Obj b -> (a ** b) ~> (b ** a)
forall k (a :: k) (b :: k).
SymMonoidal k =>
Obj a -> Obj b -> (a ** b) ~> (b ** a)
swap' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)

isObPar :: forall {k} a b r. (Monoidal k, Ob (a :: k), Ob b) => (Ob (a ** b) => r) -> r
isObPar :: forall {k} (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
isObPar Ob (a ** b) => r
r = r
Ob (a ** b) => r
(Ob (a ** b), Ob (a ** b)) => r
r ((Ob (a ** b), Ob (a ** b)) => r) -> ((a ** b) ~> (a ** b)) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (b ~> b) -> (a ** b) ~> (a ** b)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)

first :: forall {k} c a b. (Monoidal k, Ob (c :: k)) => (a ~> b) -> (a ** c) ~> (b ** c)
first :: forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first a ~> b
f = a ~> b
f (a ~> b) -> (c ~> c) -> (a ** c) ~> (b ** c)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c

second :: forall {k} c a b. (Monoidal k, Ob (c :: k)) => (a ~> b) -> (c ** a) ~> (c ** b)
second :: forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
second a ~> b
f = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj c -> (a ~> b) -> (c ** a) ~> (c ** b)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` a ~> b
f


type family (as :: [k]) ++ (bs :: [k]) :: [k] where
  '[] ++ bs = bs
  (a ': as) ++ bs = a ': (as ++ bs)

data SList as where
  Nil :: SList '[]
  Cons :: (Ob a, Ob as) => Obj a -> SList as -> SList (a ': as)

type IsList :: forall {k}. [k] -> Constraint
class CategoryOf k => IsList (as :: [k]) where sList :: SList as
instance CategoryOf k => IsList ('[] :: [k]) where sList :: SList '[]
sList = SList '[]
forall {k}. SList '[]
Nil
instance (Ob a, Ob as) => IsList (a ': as) where sList :: SList (a : as)
sList = Obj a -> SList as -> SList (a : as)
forall {k} (a :: k) (as :: [k]).
(Ob a, Ob as) =>
Obj a -> SList as -> SList (a : as)
Cons (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @as)

type family Fold (as :: [k]) :: k where
  Fold ('[] :: [k]) = Unit :: k
  Fold '[a] = a
  Fold (a ': as) = a ** Fold as

fold :: forall {k} as. Monoidal k => SList (as :: [k]) -> Fold as ~> Fold as
fold :: forall {k} (as :: [k]).
Monoidal k =>
SList as -> Fold as ~> Fold as
fold SList as
Nil = Fold as ~> Fold as
Unit ~> Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
fold (Cons Obj a
f SList as
Nil) = Obj a
Fold as ~> Fold as
f
fold (Cons Obj a
f fs :: SList as
fs@Cons{}) = Obj a
f Obj a
-> (Fold (a : as) ~> Fold (a : as))
-> (a ** Fold (a : as)) ~> (a ** Fold (a : as))
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` SList as -> Fold as ~> Fold as
forall {k} (as :: [k]).
Monoidal k =>
SList as -> Fold as ~> Fold as
fold SList as
fs

concatFold
  :: forall {k} (as :: [k]) (bs :: [k]). (Ob as, Ob bs, Monoidal k)
  => Fold as ** Fold bs ~> Fold (as ++ bs)
concatFold :: forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs, Monoidal k) =>
(Fold as ** Fold bs) ~> Fold (as ++ bs)
concatFold =
  let fbs :: Fold bs ~> Fold bs
fbs = SList bs -> Fold bs ~> Fold bs
forall {k} (as :: [k]).
Monoidal k =>
SList as -> Fold as ~> Fold as
fold (forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @bs)
      h :: forall (cs :: [k]). SList cs -> (Fold cs ** Fold bs) ~> Fold (cs ++ bs)
      h :: forall (cs :: [k]).
SList cs -> (Fold cs ** Fold bs) ~> Fold (cs ++ bs)
h SList cs
Nil = (Fold bs ~> Fold bs) -> (Unit ** Fold bs) ~> Fold bs
forall (a :: k). Obj a -> (Unit ** a) ~> a
forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a
leftUnitor Fold bs ~> Fold bs
fbs
      h (Cons Obj a
c SList as
Nil) = case forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @bs of
        SList bs
Nil -> Obj a -> (a ** Unit) ~> a
forall (a :: k). Obj a -> (a ** Unit) ~> a
forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a
rightUnitor Obj a
c
        Cons{} -> Obj a
c Obj a
-> (Fold (a : as) ~> Fold (a : as))
-> (a ** Fold (a : as)) ~> (a ** Fold (a : as))
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Fold bs ~> Fold bs
Fold (a : as) ~> Fold (a : as)
fbs
      h (Cons Obj a
c cs :: SList as
cs@Cons{}) = (Obj a
c Obj a
-> ((Fold (a : as) ** Fold bs) ~> Fold (a : (as ++ bs)))
-> (a ** (Fold (a : as) ** Fold bs))
   ~> (a ** Fold (a : (as ++ bs)))
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` SList as -> (Fold as ** Fold bs) ~> Fold (as ++ bs)
forall (cs :: [k]).
SList cs -> (Fold cs ** Fold bs) ~> Fold (cs ++ bs)
h SList as
cs) ((a ** (Fold (a : as) ** Fold bs)) ~> (a ** Fold (a : (as ++ bs))))
-> (((a ** Fold (a : as)) ** Fold bs)
    ~> (a ** (Fold (a : as) ** Fold bs)))
-> ((a ** Fold (a : as)) ** Fold bs)
   ~> (a ** Fold (a : (as ++ bs)))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj a
-> Obj (Fold (a : as))
-> (Fold bs ~> Fold bs)
-> ((a ** Fold (a : as)) ** Fold bs)
   ~> (a ** (Fold (a : as) ** Fold bs))
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Obj a
c (SList as -> Fold as ~> Fold as
forall {k} (as :: [k]).
Monoidal k =>
SList as -> Fold as ~> Fold as
fold SList as
cs) Fold bs ~> Fold bs
fbs
  in SList as -> (Fold as ** Fold bs) ~> Fold (as ++ bs)
forall (cs :: [k]).
SList cs -> (Fold cs ** Fold bs) ~> Fold (cs ++ bs)
h (forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @as)

splitFold
  :: forall {k} (as :: [k]) (bs :: [k]). (Ob as, Ob bs, Monoidal k)
  => Fold (as ++ bs) ~> (Fold as ** Fold bs)
splitFold :: forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs, Monoidal k) =>
Fold (as ++ bs) ~> (Fold as ** Fold bs)
splitFold =
  let fbs :: Fold bs ~> Fold bs
fbs = SList bs -> Fold bs ~> Fold bs
forall {k} (as :: [k]).
Monoidal k =>
SList as -> Fold as ~> Fold as
fold (forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @bs)
      h :: forall cs. SList cs -> Fold (cs ++ bs) ~> Fold cs ** Fold bs
      h :: forall (cs :: [k]).
SList cs -> Fold (cs ++ bs) ~> (Fold cs ** Fold bs)
h SList cs
Nil = (Fold bs ~> Fold bs) -> Fold bs ~> (Unit ** Fold bs)
forall (a :: k). Obj a -> a ~> (Unit ** a)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
leftUnitorInv Fold bs ~> Fold bs
fbs
      h (Cons Obj a
c SList as
Nil) = case forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @bs of
        SList bs
Nil -> Obj a -> a ~> (a ** Unit)
forall (a :: k). Obj a -> a ~> (a ** Unit)
forall k (a :: k). Monoidal k => Obj a -> a ~> (a ** Unit)
rightUnitorInv Obj a
c
        Cons{} -> Obj a
c Obj a
-> (Fold (a : as) ~> Fold (a : as))
-> (a ** Fold (a : as)) ~> (a ** Fold (a : as))
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Fold bs ~> Fold bs
Fold (a : as) ~> Fold (a : as)
fbs
      h (Cons Obj a
c cs :: SList as
cs@Cons{}) = Obj a
-> Obj (Fold (a : as))
-> (Fold bs ~> Fold bs)
-> (a ** (Fold (a : as) ** Fold bs))
   ~> ((a ** Fold (a : as)) ** Fold bs)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj a
c (SList as -> Fold as ~> Fold as
forall {k} (as :: [k]).
Monoidal k =>
SList as -> Fold as ~> Fold as
fold SList as
cs) Fold bs ~> Fold bs
fbs ((a ** (Fold (a : as) ** Fold bs))
 ~> ((a ** Fold (a : as)) ** Fold bs))
-> ((a ** Fold (a : (as ++ bs)))
    ~> (a ** (Fold (a : as) ** Fold bs)))
-> (a ** Fold (a : (as ++ bs)))
   ~> ((a ** Fold (a : as)) ** Fold bs)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Obj a
c Obj a
-> (Fold (a : (as ++ bs)) ~> (Fold (a : as) ** Fold bs))
-> (a ** Fold (a : (as ++ bs)))
   ~> (a ** (Fold (a : as) ** Fold bs))
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` SList as -> Fold (as ++ bs) ~> (Fold as ** Fold bs)
forall (cs :: [k]).
SList cs -> Fold (cs ++ bs) ~> (Fold cs ** Fold bs)
h SList as
cs)
  in SList as -> Fold (as ++ bs) ~> (Fold as ** Fold bs)
forall (cs :: [k]).
SList cs -> Fold (cs ++ bs) ~> (Fold cs ** Fold bs)
h (forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @as)


type Strictified :: CAT [k]
data Strictified as bs where
  Str :: (Ob as, Ob bs) => Fold as ~> Fold bs -> Strictified as bs

singleton :: CategoryOf k => Obj (a :: k) -> Obj '[a]
singleton :: forall k (a :: k). CategoryOf k => Obj a -> Obj '[a]
singleton Obj a
a = (Fold '[a] ~> Fold '[a]) -> Strictified '[a] '[a]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str Obj a
Fold '[a] ~> Fold '[a]
a ((Ob a, Ob a) => Strictified '[a] '[a])
-> Obj a -> Strictified '[a] '[a]
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Obj a
a

instance Monoidal k => Profunctor (Strictified :: CAT [k]) where
  dimap :: forall (c :: [k]) (a :: [k]) (b :: [k]) (d :: [k]).
(c ~> a) -> (b ~> d) -> Strictified a b -> Strictified c d
dimap = (c ~> a) -> (b ~> d) -> Strictified a b -> Strictified c d
Strictified c a
-> Strictified b d -> Strictified a b -> Strictified c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: [k]) (b :: [k]) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
\\ Str Fold a ~> Fold b
f = r
(Ob (Fold a), Ob (Fold b)) => r
(Ob a, Ob b) => r
r ((Ob (Fold a), Ob (Fold b)) => r) -> (Fold a ~> Fold b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Fold a ~> Fold b
f

instance Monoidal k => Promonad (Strictified :: CAT [k]) where
  id :: forall (as :: [k]). Ob as => Strictified as as
  id :: forall (a :: [k]). Ob a => Strictified a a
id = (Fold as ~> Fold as) -> Strictified as as
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (SList as -> Fold as ~> Fold as
forall {k} (as :: [k]).
Monoidal k =>
SList as -> Fold as ~> Fold as
fold (forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @as))
  Str Fold b ~> Fold c
f . :: forall (b :: [k]) (c :: [k]) (a :: [k]).
Strictified b c -> Strictified a b -> Strictified a c
. Str Fold a ~> Fold b
g = (Fold a ~> Fold c) -> Strictified a c
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (Fold b ~> Fold c
f (Fold b ~> Fold c) -> (Fold a ~> Fold b) -> Fold a ~> Fold c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Fold a ~> Fold b
g)

instance Monoidal k => CategoryOf [k] where
  type (~>) = Strictified
  type Ob as = IsList as

instance Monoidal k => Monoidal [k] where
  type Unit = '[]
  type as ** bs = as ++ bs
  par :: (as :: [k]) ~> bs -> cs ~> ds -> as ++ cs ~> bs ++ ds
  par :: forall (as :: [k]) (bs :: [k]) (cs :: [k]) (ds :: [k]).
(as ~> bs) -> (cs ~> ds) -> (as ++ cs) ~> (bs ++ ds)
par (Str @as @bs Fold as ~> Fold bs
f) (Str @cs @ds Fold cs ~> Fold ds
g) =
    forall (a :: [k]) (b :: [k]) r.
(Monoidal [k], Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
forall {k} (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
isObPar @as @cs ((Ob (as ** cs) => (as ++ cs) ~> (bs ++ ds))
 -> (as ++ cs) ~> (bs ++ ds))
-> (Ob (as ** cs) => (as ++ cs) ~> (bs ++ ds))
-> (as ++ cs) ~> (bs ++ ds)
forall a b. (a -> b) -> a -> b
$ forall (a :: [k]) (b :: [k]) r.
(Monoidal [k], Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
forall {k} (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
isObPar @bs @ds ((Ob (bs ** ds) => (as ++ cs) ~> (bs ++ ds))
 -> (as ++ cs) ~> (bs ++ ds))
-> (Ob (bs ** ds) => (as ++ cs) ~> (bs ++ ds))
-> (as ++ cs) ~> (bs ++ ds)
forall a b. (a -> b) -> a -> b
$
      (Fold (as ++ cs) ~> Fold (bs ++ ds))
-> Strictified (as ++ cs) (bs ++ ds)
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs, Monoidal k) =>
(Fold as ** Fold bs) ~> Fold (as ++ bs)
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs, Monoidal k) =>
(Fold as ** Fold bs) ~> Fold (as ++ bs)
concatFold @bs @ds ((Fold bs ** Fold ds) ~> Fold (bs ++ ds))
-> (Fold (as ++ cs) ~> (Fold bs ** Fold ds))
-> Fold (as ++ cs) ~> Fold (bs ++ ds)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Fold as ~> Fold bs
f (Fold as ~> Fold bs)
-> (Fold cs ~> Fold ds)
-> (Fold as ** Fold cs) ~> (Fold bs ** Fold ds)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Fold cs ~> Fold ds
g) ((Fold as ** Fold cs) ~> (Fold bs ** Fold ds))
-> (Fold (as ++ cs) ~> (Fold as ** Fold cs))
-> Fold (as ++ cs) ~> (Fold bs ** Fold ds)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs, Monoidal k) =>
Fold (as ++ bs) ~> (Fold as ** Fold bs)
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs, Monoidal k) =>
Fold (as ++ bs) ~> (Fold as ** Fold bs)
splitFold @as @cs)
  leftUnitor :: forall (a :: [k]). Obj a -> (Unit ** a) ~> a
leftUnitor Obj a
a = Obj a
(Unit ** a) ~> a
a
  leftUnitorInv :: forall (a :: [k]). Obj a -> a ~> (Unit ** a)
leftUnitorInv Obj a
a = Obj a
a ~> (Unit ** a)
a
  rightUnitor :: forall as. Obj (as :: [k]) -> as ** Unit ~> as
  rightUnitor :: forall (a :: [k]). Obj a -> (a ** Unit) ~> a
rightUnitor Obj as
as' = SList as -> (as ** Unit) ~> as
forall (bs :: [k]). SList bs -> (bs ** Unit) ~> bs
go (forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @as) ((Ob as, Ob as) => Strictified (as ++ '[]) as)
-> Strictified as as -> Strictified (as ++ '[]) as
forall (a :: [k]) (b :: [k]) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Obj as
Strictified as as
as' where
    go :: forall (bs :: [k]). SList bs -> bs ** Unit ~> bs
    go :: forall (bs :: [k]). SList bs -> (bs ** Unit) ~> bs
go SList bs
Nil = (bs ** Unit) ~> bs
Strictified '[] '[]
forall (a :: [k]). Ob a => Strictified a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
    go (Cons Obj a
_ SList as
Nil) = (bs ** Unit) ~> bs
Strictified '[a] '[a]
forall (a :: [k]). Ob a => Strictified a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
    go (Cons Obj a
a as :: SList as
as@Cons{}) = Obj a -> '[a] ~> '[a]
forall k (a :: k). CategoryOf k => Obj a -> Obj '[a]
singleton Obj a
a ('[a] ~> '[a])
-> ((a : (as ++ '[])) ~> (a : as))
-> ('[a] ** (a : (as ++ '[]))) ~> ('[a] ** (a : as))
forall (a :: [k]) (b :: [k]) (c :: [k]) (d :: [k]).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` SList as -> (as ** Unit) ~> as
forall (bs :: [k]). SList bs -> (bs ** Unit) ~> bs
go SList as
as
  rightUnitorInv :: forall as. Obj (as :: [k]) -> as ~> as ** Unit
  rightUnitorInv :: forall (a :: [k]). Obj a -> a ~> (a ** Unit)
rightUnitorInv Obj as
as' = SList as -> as ~> (as ** Unit)
forall (bs :: [k]). SList bs -> bs ~> (bs ** Unit)
go (forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @as) ((Ob as, Ob as) => Strictified as (as ++ '[]))
-> Strictified as as -> Strictified as (as ++ '[])
forall (a :: [k]) (b :: [k]) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Obj as
Strictified as as
as' where
    go :: forall (bs :: [k]). SList bs -> bs ~> bs ** Unit
    go :: forall (bs :: [k]). SList bs -> bs ~> (bs ** Unit)
go SList bs
Nil = bs ~> (bs ** Unit)
Strictified '[] '[]
forall (a :: [k]). Ob a => Strictified a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
    go (Cons Obj a
_ SList as
Nil) = bs ~> (bs ** Unit)
Strictified '[a] '[a]
forall (a :: [k]). Ob a => Strictified a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
    go (Cons Obj a
a as :: SList as
as@Cons{}) = Obj a -> '[a] ~> '[a]
forall k (a :: k). CategoryOf k => Obj a -> Obj '[a]
singleton Obj a
a ('[a] ~> '[a])
-> ((a : as) ~> (a : (as ++ '[])))
-> ('[a] ** (a : as)) ~> ('[a] ** (a : (as ++ '[])))
forall (a :: [k]) (b :: [k]) (c :: [k]) (d :: [k]).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` SList as -> as ~> (as ** Unit)
forall (bs :: [k]). SList bs -> bs ~> (bs ** Unit)
go SList as
as
  associator :: forall as bs cs. Obj (as :: [k]) -> Obj bs -> Obj cs -> (as ** bs) ** cs ~> as ** (bs ** cs)
  associator :: forall (a :: [k]) (b :: [k]) (c :: [k]).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Obj as
as' Obj bs
bs' Obj cs
cs' = SList as -> ((as ** bs) ** cs) ~> (as ** (bs ** cs))
forall (as' :: [k]).
SList as' -> ((as' ** bs) ** cs) ~> (as' ** (bs ** cs))
go (forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @as) ((Ob as, Ob as) =>
 Strictified ((as ++ bs) ++ cs) (as ++ (bs ++ cs)))
-> Strictified as as
-> Strictified ((as ++ bs) ++ cs) (as ++ (bs ++ cs))
forall (a :: [k]) (b :: [k]) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Obj as
Strictified as as
as' where
    go :: forall (as' :: [k]). SList as' -> (as' ** bs) ** cs ~> as' ** (bs ** cs)
    go :: forall (as' :: [k]).
SList as' -> ((as' ** bs) ** cs) ~> (as' ** (bs ** cs))
go SList as'
Nil = Obj bs
bs' Obj bs -> Obj cs -> (bs ** cs) ~> (bs ** cs)
forall (a :: [k]) (b :: [k]) (c :: [k]) (d :: [k]).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj cs
cs'
    go (Cons Obj a
a SList as
Nil) = Obj a -> '[a] ~> '[a]
forall k (a :: k). CategoryOf k => Obj a -> Obj '[a]
singleton Obj a
a ('[a] ~> '[a])
-> ((bs ++ cs) ~> (bs ++ cs))
-> ('[a] ** (bs ++ cs)) ~> ('[a] ** (bs ++ cs))
forall (a :: [k]) (b :: [k]) (c :: [k]) (d :: [k]).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` (Obj bs
bs' Obj bs -> Obj cs -> (bs ** cs) ~> (bs ** cs)
forall (a :: [k]) (b :: [k]) (c :: [k]) (d :: [k]).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj cs
cs')
    go (Cons Obj a
a as :: SList as
as@Cons{}) = Obj a -> '[a] ~> '[a]
forall k (a :: k). CategoryOf k => Obj a -> Obj '[a]
singleton Obj a
a ('[a] ~> '[a])
-> ((a : ((as ++ bs) ++ cs)) ~> (a : (as ++ (bs ++ cs))))
-> ('[a] ** (a : ((as ++ bs) ++ cs)))
   ~> ('[a] ** (a : (as ++ (bs ++ cs))))
forall (a :: [k]) (b :: [k]) (c :: [k]) (d :: [k]).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` SList as -> ((as ** bs) ** cs) ~> (as ** (bs ** cs))
forall (as' :: [k]).
SList as' -> ((as' ** bs) ** cs) ~> (as' ** (bs ** cs))
go SList as
as
  associatorInv :: forall as bs cs. Obj (as :: [k]) -> Obj bs -> Obj cs -> as ** (bs ** cs) ~> (as ** bs) ** cs
  associatorInv :: forall (a :: [k]) (b :: [k]) (c :: [k]).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj as
as' Obj bs
bs' Obj cs
cs' = SList as -> (as ** (bs ** cs)) ~> ((as ** bs) ** cs)
forall (as' :: [k]).
SList as' -> (as' ** (bs ** cs)) ~> ((as' ** bs) ** cs)
go (forall (as :: [k]). IsList as => SList as
forall {k} (as :: [k]). IsList as => SList as
sList @as) ((Ob as, Ob as) =>
 Strictified (as ++ (bs ++ cs)) ((as ++ bs) ++ cs))
-> Strictified as as
-> Strictified (as ++ (bs ++ cs)) ((as ++ bs) ++ cs)
forall (a :: [k]) (b :: [k]) r.
((Ob a, Ob b) => r) -> Strictified a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Obj as
Strictified as as
as' where
    go :: forall (as' :: [k]). SList as' -> as' ** (bs ** cs) ~> (as' ** bs) ** cs
    go :: forall (as' :: [k]).
SList as' -> (as' ** (bs ** cs)) ~> ((as' ** bs) ** cs)
go SList as'
Nil = Obj bs
bs' Obj bs -> Obj cs -> (bs ** cs) ~> (bs ** cs)
forall (a :: [k]) (b :: [k]) (c :: [k]) (d :: [k]).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj cs
cs'
    go (Cons Obj a
a SList as
Nil) = Obj a -> '[a] ~> '[a]
forall k (a :: k). CategoryOf k => Obj a -> Obj '[a]
singleton Obj a
a ('[a] ~> '[a])
-> ((bs ++ cs) ~> (bs ++ cs))
-> ('[a] ** (bs ++ cs)) ~> ('[a] ** (bs ++ cs))
forall (a :: [k]) (b :: [k]) (c :: [k]) (d :: [k]).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` (Obj bs
bs' Obj bs -> Obj cs -> (bs ** cs) ~> (bs ** cs)
forall (a :: [k]) (b :: [k]) (c :: [k]) (d :: [k]).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj cs
cs')
    go (Cons Obj a
a as :: SList as
as@Cons{}) = Obj a -> '[a] ~> '[a]
forall k (a :: k). CategoryOf k => Obj a -> Obj '[a]
singleton Obj a
a ('[a] ~> '[a])
-> ((a : (as ++ (bs ++ cs))) ~> (a : ((as ++ bs) ++ cs)))
-> ('[a] ** (a : (as ++ (bs ++ cs))))
   ~> ('[a] ** (a : ((as ++ bs) ++ cs)))
forall (a :: [k]) (b :: [k]) (c :: [k]) (d :: [k]).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` SList as -> (as ** (bs ** cs)) ~> ((as ** bs) ** cs)
forall (as' :: [k]).
SList as' -> (as' ** (bs ** cs)) ~> ((as' ** bs) ** cs)
go SList as
as

-- instance SymMonoidal k => SymMonoidal [k] where
--   swap :: forall k (as :: [k]) (bs :: [k]). SymMonoidal k => Obj as -> Obj bs -> (as ** bs) ~> (bs ** as)
--   swap as bs = go (sList @as) (sList @bs) \\ as \\ bs
--     where
--       go :: forall (as' :: [k]) bs'. SList as' -> SList bs' -> (as' ** bs') ~> (bs' ** as')
--       go as Nil = rightUnitor _
--       go Nil bs = rightUnitorInv _
--       go (Cons a as) (Cons b bs) = _
--       swap1 :: Obj (a :: k) -> SList (as :: [k]) -> (a ': as) ~> (as ++ '[a])
--       swap1 = swap1


class (Monoidal j, Monoidal k, Profunctor p) => MonoidalProfunctor (p :: PRO j k) where
  lift0 :: p Unit Unit
  lift2 :: p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)

newtype Hom a b = Hom { forall {k} (a :: k) (b :: k). Hom a b -> a ~> b
getHom :: a ~> b }
instance CategoryOf k => Profunctor (Hom :: PRO k k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Hom a b -> Hom c d
dimap c ~> a
l b ~> d
r (Hom a ~> b
f) = (c ~> d) -> Hom c d
forall {k} (a :: k) (b :: k). (a ~> b) -> Hom a b
Hom ((c ~> a) -> (b ~> d) -> (a ~> b) -> c ~> d
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> (a ~> b) -> c ~> d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l b ~> d
r a ~> b
f)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> Hom a b -> r
\\ Hom a ~> b
f = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
instance Monoidal k => MonoidalProfunctor (Hom :: PRO k k) where
  lift0 :: Hom Unit Unit
lift0 = (Unit ~> Unit) -> Hom Unit Unit
forall {k} (a :: k) (b :: k). (a ~> b) -> Hom a b
Hom Unit ~> Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  lift2 :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Hom x1 x2 -> Hom y1 y2 -> Hom (x1 ** y1) (x2 ** y2)
lift2 (Hom x1 ~> x2
f) (Hom y1 ~> y2
g) = ((x1 ** y1) ~> (x2 ** y2)) -> Hom (x1 ** y1) (x2 ** y2)
forall {k} (a :: k) (b :: k). (a ~> b) -> Hom a b
Hom (x1 ~> x2
f (x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` y1 ~> y2
g)