{-# 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 (..), SymMonoidal (..), associatorInv', associator')
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 :: 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
  SNil :: SList '[]
  SSing :: (Ob a) => SList '[a]
  SCons :: (Ob a, Ob as, Ob bs, as ~ b ': bs) => 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
  withIsList2 :: IsList bs => (IsList (as ++ bs) => r) -> r
  swap1 :: (Ob b, SymMonoidal k) => as ++ '[b] ~> b ': as
  swap1Inv :: (Ob b, SymMonoidal k) => b ': as ~> as ++ '[b]
  swap' :: (IsList (bs :: [k]), SymMonoidal k) => as ++ bs ~> bs ++ as
instance (CategoryOf k) => IsList ('[] :: [k]) where
  sList :: SList '[]
sList = SList '[]
forall {a :: Kind}. SList '[]
SNil
  withIsList2 :: forall (bs :: [k]) (r :: Kind).
IsList bs =>
(IsList ('[] ++ bs) => r) -> r
withIsList2 IsList ('[] ++ bs) => r
r = r
IsList ('[] ++ bs) => r
r
  swap1 :: forall (b :: k). (Ob b, SymMonoidal k) => ('[] ++ '[b]) ~> '[b]
swap1 = ('[] ++ '[b]) ~> '[b]
Strictified '[b] '[b]
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
  swap1Inv :: forall (b :: k). (Ob b, SymMonoidal k) => '[b] ~> ('[] ++ '[b])
swap1Inv = '[b] ~> ('[] ++ '[b])
Strictified '[b] '[b]
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
  swap' :: forall (bs :: [k]).
(IsList bs, SymMonoidal k) =>
('[] ++ bs) ~> (bs ++ '[])
swap' = ('[] ++ bs) ~> (bs ++ '[])
Strictified bs bs
forall (a :: [k]). Ob a => Strictified a a
forall {k :: Kind} (p :: k +-> k) (a :: k).
(Promonad p, Ob a) =>
p a a
id
instance (Ob (a :: k), CategoryOf k) => IsList '[a] where
  sList :: SList '[a]
sList = SList '[a]
forall {a :: Kind} (a :: a). Ob a => SList '[a]
SSing
  withIsList2 :: forall (bs :: [k]) (r :: Kind).
IsList bs =>
(IsList ('[a] ++ bs) => r) -> r
withIsList2 @bs IsList ('[a] ++ bs) => r
r = case forall (as :: [k]). IsList as => SList as
forall {k :: Kind} (as :: [k]). IsList as => SList as
sList @bs of SList bs
SNil -> r
IsList ('[a] ++ bs) => r
r; SList bs
SSing -> r
IsList ('[a] ++ bs) => r
r; SList bs
SCons -> r
IsList ('[a] ++ bs) => r
r
  swap1 :: forall (b :: k). (Ob b, SymMonoidal k) => ('[a] ++ '[b]) ~> '[b, a]
swap1 @b = (Fold '[a, b] ~> Fold '[b, a]) -> Strictified '[a, b] '[b, a]
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall (k :: Kind) (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @b)
  swap1Inv :: forall (b :: k). (Ob b, SymMonoidal k) => '[b, a] ~> ('[a] ++ '[b])
swap1Inv @b = (Fold '[b, a] ~> Fold '[a, b]) -> Strictified '[b, a] '[a, b]
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall (k :: Kind) (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @b @a)
  swap' :: forall (bs :: [k]).
(IsList bs, SymMonoidal k) =>
('[a] ++ bs) ~> (bs ++ '[a])
swap' @bs = forall (as :: [k]) (b :: k).
(IsList as, Ob b, SymMonoidal k) =>
(b : as) ~> (as ++ '[b])
forall {k :: Kind} (as :: [k]) (b :: k).
(IsList as, Ob b, SymMonoidal k) =>
(b : as) ~> (as ++ '[b])
swap1Inv @bs @a
instance (Ob (a1 :: k), IsList (a2 ': as), IsList as) => IsList (a1 ': a2 ': as) where
  sList :: SList (a1 : a2 : as)
sList = SList (a1 : a2 : as)
forall {a :: Kind} (a :: a) (as :: [a]) (bs :: [a]) (b :: a).
(Ob a, Ob as, Ob bs, as ~ (b : bs)) =>
SList (a : as)
SCons
  withIsList2 :: forall (bs :: [k]) (r :: Kind).
IsList bs =>
(IsList ((a1 : a2 : as) ++ bs) => r) -> r
withIsList2 @bs IsList ((a1 : a2 : as) ++ bs) => r
r = forall (as :: [k]) (bs :: [k]) (r :: Kind).
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k :: Kind} (as :: [k]) (bs :: [k]) (r :: Kind).
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
withIsList2 @(a2 ': as) @bs ((IsList ((a2 : as) ++ bs) => r) -> r)
-> (IsList ((a2 : as) ++ bs) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall (as :: [k]) (bs :: [k]) (r :: Kind).
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k :: Kind} (as :: [k]) (bs :: [k]) (r :: Kind).
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
withIsList2 @as @bs r
IsList (as ++ bs) => r
IsList ((a1 : a2 : as) ++ bs) => r
r
  swap1 :: forall (b :: k).
(Ob b, SymMonoidal k) =>
((a1 : a2 : as) ++ '[b]) ~> (b : a1 : a2 : as)
swap1 @b = case forall (as :: [k]) (b :: k).
(IsList as, Ob b, SymMonoidal k) =>
(as ++ '[b]) ~> (b : as)
forall {k :: Kind} (as :: [k]) (b :: k).
(IsList as, Ob b, SymMonoidal k) =>
(as ++ '[b]) ~> (b : as)
swap1 @(a2 ': as) @b of ((a2 : as) ++ '[b]) ~> (b : a2 : as)
f -> (forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[a1, b] @[b, a1] (forall (k :: Kind) (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @a1 @b) Strictified '[a1, b] '[b, a1]
-> Strictified (a2 : as) (a2 : as)
-> Strictified ('[a1, b] ** (a2 : as)) ('[b, a1] ** (a2 : 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` forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(a2 ': as)) Strictified (a1 : b : a2 : as) (b : a1 : a2 : as)
-> Strictified (a1 : a2 : (as ++ '[b])) (a1 : b : a2 : as)
-> Strictified (a1 : a2 : (as ++ '[b])) (b : a1 : a2 : as)
forall (b :: [k]) (c :: [k]) (a :: [k]).
Strictified b c -> Strictified a b -> Strictified a c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[a1] Strictified '[a1] '[a1]
-> Strictified (a2 : (as ++ '[b])) (b : a2 : as)
-> Strictified
     ('[a1] ** (a2 : (as ++ '[b]))) ('[a1] ** (b : a2 : 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` ((a2 : as) ++ '[b]) ~> (b : a2 : as)
Strictified (a2 : (as ++ '[b])) (b : a2 : as)
f)
  swap1Inv :: forall (b :: k).
(Ob b, SymMonoidal k) =>
(b : a1 : a2 : as) ~> ((a1 : a2 : as) ++ '[b])
swap1Inv @b = case forall (as :: [k]) (b :: k).
(IsList as, Ob b, SymMonoidal k) =>
(b : as) ~> (as ++ '[b])
forall {k :: Kind} (as :: [k]) (b :: k).
(IsList as, Ob b, SymMonoidal k) =>
(b : as) ~> (as ++ '[b])
swap1Inv @(a2 ': as) @b of (b : a2 : as) ~> ((a2 : as) ++ '[b])
f -> (forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[a1] Strictified '[a1] '[a1]
-> Strictified (b : a2 : as) (a2 : (as ++ '[b]))
-> Strictified
     ('[a1] ** (b : a2 : as)) ('[a1] ** (a2 : (as ++ '[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` (b : a2 : as) ~> ((a2 : as) ++ '[b])
Strictified (b : a2 : as) (a2 : (as ++ '[b]))
f) Strictified ('[a1] ++ (b : a2 : as)) (a1 : a2 : (as ++ '[b]))
-> Strictified (b : a1 : a2 : as) ('[a1] ++ (b : a2 : as))
-> Strictified (b : a1 : a2 : as) (a1 : a2 : (as ++ '[b]))
forall (b :: [k]) (c :: [k]) (a :: [k]).
Strictified b c -> Strictified a b -> Strictified a c
forall {k :: Kind} (p :: 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) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[b, a1] @[a1, b] (forall (k :: Kind) (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @b @a1) Strictified '[b, a1] '[a1, b]
-> Strictified (a2 : as) (a2 : as)
-> Strictified ('[b, a1] ** (a2 : as)) ('[a1, b] ** (a2 : 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` forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(a2 ': as))
  swap' :: forall (bs :: [k]).
(IsList bs, SymMonoidal k) =>
((a1 : a2 : as) ++ bs) ~> (bs ++ (a1 : a2 : as))
swap' @bs = case forall (as :: [k]) (bs :: [k]).
(IsList as, IsList bs, SymMonoidal k) =>
(as ++ bs) ~> (bs ++ as)
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(IsList as, IsList bs, SymMonoidal k) =>
(as ++ bs) ~> (bs ++ as)
swap' @(a2 ': as) @bs of ((a2 : as) ++ bs) ~> (bs ++ (a2 : as))
f -> forall (k :: Kind) (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @bs @'[a1] @(a2 ': as) Strictified ((bs ++ '[a1]) ++ (a2 : as)) (bs ++ (a1 : a2 : as))
-> Strictified (a1 : a2 : (as ++ bs)) ((bs ++ '[a1]) ++ (a2 : as))
-> Strictified (a1 : a2 : (as ++ bs)) (bs ++ (a1 : a2 : as))
forall (b :: [k]) (c :: [k]) (a :: [k]).
Strictified b c -> Strictified a b -> Strictified a c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (as :: [k]) (b :: k).
(IsList as, Ob b, SymMonoidal k) =>
(b : as) ~> (as ++ '[b])
forall {k :: Kind} (as :: [k]) (b :: k).
(IsList as, Ob b, SymMonoidal k) =>
(b : as) ~> (as ++ '[b])
swap1Inv @bs @a1 Strictified (a1 : bs) (bs ++ '[a1])
-> Strictified (a2 : as) (a2 : as)
-> Strictified
     ((a1 : bs) ** (a2 : as)) ((bs ++ '[a1]) ** (a2 : 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` forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(a2 ': as)) Strictified ((a1 : bs) ++ (a2 : as)) ((bs ++ '[a1]) ++ (a2 : as))
-> Strictified (a1 : a2 : (as ++ bs)) ((a1 : bs) ++ (a2 : as))
-> Strictified (a1 : a2 : (as ++ bs)) ((bs ++ '[a1]) ++ (a2 : as))
forall (b :: [k]) (c :: [k]) (a :: [k]).
Strictified b c -> Strictified a b -> Strictified a c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[a1] Strictified '[a1] '[a1]
-> Strictified (a2 : (as ++ bs)) (bs ++ (a2 : as))
-> Strictified
     ('[a1] ** (a2 : (as ++ bs))) ('[a1] ** (bs ++ (a2 : 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` ((a2 : as) ++ bs) ~> (bs ++ (a2 : as))
Strictified (a2 : (as ++ bs)) (bs ++ (a2 : as))
f)

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
SNil = Unit ~> Unit
Fold as ~> Fold as
forall {j :: Kind} {k :: Kind} (p :: j +-> k).
MonoidalProfunctor p =>
p Unit Unit
par0
fold (SSing @a) = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a
fold (SCons @a @as') = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a
-> (Fold (b : bs) ~> Fold (b : bs))
-> (a ** Fold (b : bs)) ~> (a ** Fold (b : 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 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')

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
SNil = (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 :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Fold bs ~> Fold bs
fbs
      h (SSing @c) = case forall (as :: [k]). IsList as => SList as
forall {k :: Kind} (as :: [k]). IsList as => SList as
sList @bs of
        SList bs
SNil -> (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
        SList bs
SSing -> forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj a -> (a ~> a) -> (a ** a) ~> (a ** a)
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` a ~> a
Fold bs ~> Fold bs
fbs
        SList bs
SCons -> forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj a
-> ((a ** Fold (b : bs)) ~> (a ** Fold (b : bs)))
-> (a ** (a ** Fold (b : bs))) ~> (a ** (a ** Fold (b : 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` (a ** Fold (b : bs)) ~> (a ** Fold (b : bs))
Fold bs ~> Fold bs
fbs
      h (SCons @c @cs') = let c :: Obj a
c = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c; cs :: SList as
cs = forall (as :: [k]). IsList as => SList as
forall {k :: Kind} (as :: [k]). IsList as => SList as
sList @cs' in (Obj a
c Obj a
-> ((Fold (b : bs) ** Fold bs) ~> Fold (b : (bs ++ bs)))
-> (a ** (Fold (b : bs) ** Fold bs))
   ~> (a ** Fold (b : (bs ++ 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 (b : bs) ** Fold bs)) ~> (a ** Fold (b : (bs ++ bs))))
-> (((a ** Fold (b : bs)) ** Fold bs)
    ~> (a ** (Fold (b : bs) ** Fold bs)))
-> ((a ** Fold (b : bs)) ** Fold bs)
   ~> (a ** Fold (b : (bs ++ bs)))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj a
-> Obj (Fold (b : bs))
-> (Fold bs ~> Fold bs)
-> ((a ** Fold (b : bs)) ** Fold bs)
   ~> (a ** (Fold (b : bs) ** 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
SNil = 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 :: j +-> k) (a :: k) (b :: j)
       (r :: Kind).
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Fold bs ~> Fold bs
fbs
      h (SSing @c) = case forall (as :: [k]). IsList as => SList as
forall {k :: Kind} (as :: [k]). IsList as => SList as
sList @bs of
        SList bs
SNil -> 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
        SList bs
SSing -> forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj a -> (a ~> a) -> (a ** a) ~> (a ** a)
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` a ~> a
Fold bs ~> Fold bs
fbs
        SList bs
SCons -> forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj a
-> ((a ** Fold (b : bs)) ~> (a ** Fold (b : bs)))
-> (a ** (a ** Fold (b : bs))) ~> (a ** (a ** Fold (b : 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` (a ** Fold (b : bs)) ~> (a ** Fold (b : bs))
Fold bs ~> Fold bs
fbs
      h (SCons @c @cs') = let c :: Obj a
c = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c; cs :: SList as
cs = forall (as :: [k]). IsList as => SList as
forall {k :: Kind} (as :: [k]). IsList as => SList as
sList @cs' in Obj a
-> Obj (Fold (b : bs))
-> (Fold bs ~> Fold bs)
-> (a ** (Fold (b : bs) ** Fold bs))
   ~> ((a ** Fold (b : bs)) ** 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 (b : bs) ** Fold bs))
 ~> ((a ** Fold (b : bs)) ** Fold bs))
-> ((a ** Fold (b : (bs ++ bs)))
    ~> (a ** (Fold (b : bs) ** Fold bs)))
-> (a ** Fold (b : (bs ++ bs)))
   ~> ((a ** Fold (b : bs)) ** Fold bs)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k :: Kind} (p :: 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 (b : (bs ++ bs)) ~> (Fold (b : bs) ** Fold bs))
-> (a ** Fold (b : (bs ++ bs)))
   ~> (a ** (Fold (b : bs) ** 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) => { forall {k :: Kind} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr :: 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 :: j +-> k) (a :: k) (b :: j)
       (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
SNil = as ~> as
Obj '[]
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj
asObj SList as
SSing = as ~> as
Obj '[a]
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj
asObj (SCons @a @as) = forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k :: Kind} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[a] Strictified '[a] '[a]
-> Strictified (b : bs) (b : bs)
-> Strictified ('[a] ** (b : bs)) ('[a] ** (b : bs))
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 @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 :: 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 :: j +-> k) (a :: k) (b :: j)
       (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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Fold a ~> Fold b
g)

-- | The strictified monoidal category, making the unitors and associators identities.
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 :: 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 (k :: Kind) (a :: k) (b :: k) (r :: Kind).
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @[k] @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 (k :: Kind) (a :: k) (b :: k) (r :: Kind).
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @[k] @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 :: 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 :: 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)

-- | List concattenation as monoidal tensor.
instance (Monoidal k) => Monoidal [k] where
  type Unit = '[]
  type as ** bs = as ++ bs
  withOb2 :: forall (a :: [k]) (b :: [k]) (r :: Kind).
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @as @bs Ob (a ** b) => r
r = forall (as :: [k]) (bs :: [k]) (r :: Kind).
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k :: Kind} (as :: [k]) (bs :: [k]) (r :: Kind).
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
withIsList2 @as @bs r
Ob (a ** b) => r
IsList (a ++ b) => r
r
  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 :: 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 :: 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 :: 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 :: 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 (a :: [k]) (b :: [k]). (Ob a, Ob b) => (a ** b) ~> (b ** a)
swap @as @bs = forall (as :: [k]) (bs :: [k]).
(IsList as, IsList bs, SymMonoidal k) =>
(as ++ bs) ~> (bs ++ as)
forall {k :: Kind} (as :: [k]) (bs :: [k]).
(IsList as, IsList bs, SymMonoidal k) =>
(as ++ bs) ~> (bs ++ as)
swap' @as @bs