{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Monoidal.Strictified where

import Data.Kind (Constraint)
import Prelude (($), type (~))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), associator', associatorInv', isObPar)
import Proarrow.Core (CAT, CategoryOf (..), Obj, Profunctor (..), Promonad (..), dimapDefault, obj)

infixl 8 ||
infixl 7 ==

(||) :: (Monoidal k) => (as :: [k]) ~> bs -> cs ~> ds -> (as ++ cs) ~> (bs ++ ds)
|| :: forall (k :: Kind) (as :: [k]) (bs :: [k]) (cs :: [k]) (ds :: [k]).
Monoidal k =>
(as ~> bs) -> (cs ~> ds) -> (as ++ cs) ~> (bs ++ ds)
(||) = (as ~> bs) -> (cs ~> ds) -> (as ++ cs) ~> (bs ++ ds)
Strictified as bs
-> Strictified cs ds -> Strictified (as ** cs) (bs ** ds)
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
par

(==) :: (CategoryOf k) => ((a :: k) ~> b) -> (b ~> c) -> a ~> c
a ~> b
f == :: forall (k :: Kind) (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== b ~> c
g = b ~> c
g (b ~> c) -> (a ~> b) -> a ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. 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)

class ((as ++ bs) ++ cs ~ as ++ (bs ++ cs)) => Assoc as bs cs
instance (as ++ (bs ++ cs) ~ (as ++ bs) ++ cs) => Assoc as bs cs

type IsList :: forall {k}. [k] -> Constraint
class (CategoryOf k, as ~ as ++ '[], forall bs cs. Assoc as bs cs) => IsList (as :: [k]) where sList :: SList as
instance (CategoryOf k) => IsList ('[] :: [k]) where sList :: SList '[]
sList = SList '[]
forall {k :: Kind}. 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 :: Kind} (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 :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall (as :: [k]). IsList as => SList as
forall {k :: Kind} (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 :: Kind} (as :: [k]).
Monoidal k =>
SList as -> Fold as ~> Fold as
fold SList as
Nil = Unit ~> Unit
Fold as ~> Fold as
forall {j :: Kind} {k :: Kind} (p :: j +-> k).
MonoidalProfunctor p =>
p Unit Unit
par0
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 (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` SList as -> Fold as ~> Fold as
forall {k :: Kind} (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 :: Kind} (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 :: Kind} (as :: [k]).
Monoidal k =>
SList as -> Fold as ~> Fold as
fold (forall (as :: [k]). IsList as => SList as
forall {k :: Kind} (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 = (Unit ** Fold bs) ~> Fold bs
(Ob (Fold bs), Ob (Fold bs)) => (Unit ** Fold bs) ~> Fold bs
forall (a :: k). Ob a => (Unit ** a) ~> a
forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((Ob (Fold bs), Ob (Fold bs)) => (Unit ** Fold bs) ~> Fold bs)
-> (Fold bs ~> Fold bs) -> (Unit ** Fold bs) ~> Fold bs
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: PRO j k) (a :: j) (b :: k)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Fold bs ~> Fold bs
fbs
      h (Cons Obj a
c SList as
Nil) = case forall (as :: [k]). IsList as => SList as
forall {k :: Kind} (as :: [k]). IsList as => SList as
sList @bs of
        SList bs
Nil -> (a ** Unit) ~> a
(Fold cs ** Fold bs) ~> Fold (cs ++ bs)
forall (a :: k). Ob a => (a ** Unit) ~> a
forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
        Cons{} -> Obj a
c Obj a
-> (Fold (a : as) ~> Fold (a : as))
-> (a ** Fold (a : as)) ~> (a ** Fold (a : as))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`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 (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`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 :: Kind} (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 {k :: Kind} (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 :: Kind} (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 :: Kind} (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 :: Kind} (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 :: Kind} (as :: [k]).
Monoidal k =>
SList as -> Fold as ~> Fold as
fold (forall (as :: [k]). IsList as => SList as
forall {k :: Kind} (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 ~> (Unit ** Fold bs)
(Ob (Fold bs), Ob (Fold bs)) => Fold bs ~> (Unit ** Fold bs)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv ((Ob (Fold bs), Ob (Fold bs)) => Fold bs ~> (Unit ** Fold bs))
-> (Fold bs ~> Fold bs) -> Fold bs ~> (Unit ** Fold bs)
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: PRO j k) (a :: j) (b :: k)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Fold bs ~> Fold bs
fbs
      h (Cons Obj a
c SList as
Nil) = case forall (as :: [k]). IsList as => SList as
forall {k :: Kind} (as :: [k]). IsList as => SList as
sList @bs of
        SList bs
Nil -> a ~> (a ** Unit)
Fold (cs ++ bs) ~> (Fold cs ** Fold bs)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall (k :: Kind) (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
        Cons{} -> Obj a
c Obj a
-> (Fold (a : as) ~> Fold (a : as))
-> (a ** Fold (a : as)) ~> (a ** Fold (a : as))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`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 {k :: Kind} (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 :: Kind} (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 :: Kind} (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 (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`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 :: Kind} (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) => (a :: k) ~> b -> '[a] ~> '[b]
singleton :: forall (k :: Kind) (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> '[a] ~> '[b]
singleton a ~> b
a = (Fold '[a] ~> Fold '[b]) -> Strictified '[a] '[b]
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str a ~> b
Fold '[a] ~> Fold '[b]
a ((Ob a, Ob b) => Strictified '[a] '[b])
-> (a ~> b) -> Strictified '[a] '[b]
forall (a :: k) (b :: k) (r :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: PRO j k) (a :: j) (b :: k)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
a

asObj :: (Monoidal k) => SList (as :: [k]) -> Obj as
asObj :: forall (k :: Kind) (as :: [k]). Monoidal k => SList as -> Obj as
asObj SList as
Nil = as ~> as
Obj '[]
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj
asObj (Cons Obj a
a SList as
as) = Obj a -> '[a] ~> '[a]
forall (k :: Kind) (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> '[a] ~> '[b]
singleton Obj a
a Strictified '[a] '[a]
-> Strictified as as -> Strictified ('[a] ** as) ('[a] ** as)
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` SList as -> Obj as
forall (k :: Kind) (as :: [k]). Monoidal k => SList as -> Obj as
asObj SList as
as

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 :: Kind} (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 :: Kind).
((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 :: Kind).
((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j :: Kind} {k :: Kind} (p :: PRO j k) (a :: j) (b :: k)
       (r :: Kind).
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 :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (SList as -> Fold as ~> Fold as
forall {k :: Kind} (as :: [k]).
Monoidal k =>
SList as -> Fold as ~> Fold as
fold (forall (as :: [k]). IsList as => SList as
forall {k :: Kind} (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 :: Kind} (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 :: Kind} (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) => MonoidalProfunctor (Strictified :: CAT [k]) where
  par0 :: Strictified Unit Unit
par0 = Strictified '[] '[]
Strictified Unit Unit
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: PRO k k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
  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 :: Kind).
(Monoidal [k], Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
forall {k :: Kind} (a :: k) (b :: k) (r :: Kind).
(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 :: Kind).
(Monoidal [k], Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
forall {k :: Kind} (a :: k) (b :: k) (r :: Kind).
(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 :: Kind} (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 :: Kind} (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 :: Kind} (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 (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`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 :: Kind} (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 :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs, Monoidal k) =>
Fold (as ++ bs) ~> (Fold as ** Fold bs)
splitFold @as @cs)

instance (Monoidal k) => Monoidal [k] where
  type Unit = '[]
  type as ** bs = as ++ bs
  leftUnitor :: forall (a :: [k]). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
Strictified a a
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: PRO k k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
  leftUnitorInv :: forall (a :: [k]). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
Strictified a a
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: PRO k k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
  rightUnitor :: forall (a :: [k]). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
Strictified a a
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: PRO k k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
  rightUnitorInv :: forall (a :: [k]). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
Strictified a a
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: PRO k k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
  associator :: forall (a :: [k]) (b :: [k]) (c :: [k]).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @as @bs @cs = forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @as Strictified a a -> Strictified b b -> Strictified (a ** b) (a ** b)
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @bs Strictified (a ++ b) (a ++ b)
-> Strictified c c -> Strictified ((a ++ b) ** c) ((a ++ b) ** c)
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @cs
  associatorInv :: forall (a :: [k]) (b :: [k]) (c :: [k]).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @as @bs @cs = forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @as Strictified a a -> Strictified b b -> Strictified (a ** b) (a ** b)
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @bs Strictified (a ++ b) (a ++ b)
-> Strictified c c -> Strictified ((a ++ b) ** c) ((a ++ b) ** c)
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
forall {j :: Kind} {k :: Kind} (p :: j +-> k) (x1 :: k) (x2 :: j)
       (y1 :: k) (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @cs

-- instance (SymMonoidal k) => SymMonoidal [k] where
--   swap' :: forall (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 (asObj as')
--       go Nil bs' = rightUnitorInv (asObj bs')
--       go (Cons a as') (Cons b bs') =
--         let sa = singleton a; sb = singleton b; sas = asObj as'; sbs = asObj bs'
--         in (singleton b `par` (associator sbs sa sas . (swap1 a bs' `par` sas) . (singleton a `par` go as' bs')))
--             . (strSwap a b `par` (sas `par` sbs))
--             . (sa `par` ((swap1Inv b as' `par` sbs) . associatorInv sas sb sbs))
--       strSwap :: Obj (a :: k) -> Obj b -> '[a, b] ~> '[b, a]
--       strSwap a b = Str (swap' a b) \\ a \\ b
--       swap1 :: forall x xs. Obj (x :: k) -> SList (xs :: [k]) -> (x ': xs) ~> (xs ++ '[x])
--       swap1 = swap1
--       swap1Inv :: forall x xs. Obj (x :: k) -> SList (xs :: [k]) -> (xs ++ '[x]) ~> (x ': xs)
--       swap1Inv = swap1Inv