{-# 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 (..), Strictly, SymMonoidal (..))
import Proarrow.Core (CAT, CategoryOf (..), Obj, Profunctor (..), Promonad (..), dimapDefault, obj)

infixl 7 ==

(==) :: (CategoryOf k) => ((a :: k) ~> b) -> (b ~> c) -> a ~> c
a ~> b
f == :: forall k (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} (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)

type IsList :: forall {k}. [k] -> Constraint
class (CategoryOf k, Obs as, Strictly as) => IsList (as :: [k]) where
  listCase
    :: ((as ~ '[]) => r)
    -> (forall a. (Ob a, as ~ '[a]) => r)
    -> (forall b bs c cs. (Ob b, Ob bs, Ob cs, as ~ (b ': bs), bs ~ (c ': cs)) => r)
    -> r
  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
  listCase :: forall r.
(('[] ~ '[]) => r)
-> (forall (a :: k). (Ob a, '[] ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, '[] ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase ('[] ~ '[]) => r
n forall (a :: k). (Ob a, '[] ~ '[a]) => r
_ forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
(Ob b, Ob bs, Ob cs, '[] ~ (b : bs), bs ~ (c : cs)) =>
r
_ = r
('[] ~ '[]) => r
n
  sList :: SList '[]
sList = SList '[]
forall {a}. SList '[]
SNil
  withIsList2 :: forall (bs :: [k]) r. 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} (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} (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} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
instance (Ob (a :: k), CategoryOf k) => IsList '[a] where
  listCase :: forall r.
(('[a] ~ '[]) => r)
-> (forall (a :: k). (Ob a, '[a] ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, '[a] ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase ('[a] ~ '[]) => r
_ forall (a :: k). (Ob a, '[a] ~ '[a]) => r
s forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
(Ob b, Ob bs, Ob cs, '[a] ~ (b : bs), bs ~ (c : cs)) =>
r
_ = r
forall (a :: k). (Ob a, '[a] ~ '[a]) => r
s
  sList :: SList '[a]
sList = SList '[a]
forall {a} (a :: a). Ob a => SList '[a]
SSing
  withIsList2 :: forall (bs :: [k]) r. IsList bs => (IsList ('[a] ++ bs) => r) -> r
withIsList2 @bs IsList ('[a] ++ bs) => r
r = forall (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @bs r
(bs ~ '[]) => r
IsList ('[a] ++ bs) => r
r r
IsList ('[a] ++ bs) => r
forall (a :: k). (Ob a, bs ~ '[a]) => r
r r
IsList ('[a] ++ bs) => r
forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
(Ob b, Ob bs, Ob cs, bs ~ (b : bs), bs ~ (c : cs)) =>
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} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall k (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} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall k (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} (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
  listCase :: forall r.
(((a1 : a2 : as) ~ '[]) => r)
-> (forall (a :: k). (Ob a, (a1 : a2 : as) ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, (a1 : a2 : as) ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase ((a1 : a2 : as) ~ '[]) => r
_ forall (a :: k). (Ob a, (a1 : a2 : as) ~ '[a]) => r
_ forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
(Ob b, Ob bs, Ob cs, (a1 : a2 : as) ~ (b : bs), bs ~ (c : cs)) =>
r
c = r
forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
(Ob b, Ob bs, Ob cs, (a1 : a2 : as) ~ (b : bs), bs ~ (c : cs)) =>
r
c
  sList :: SList (a1 : a2 : as)
sList = SList (a1 : a2 : as)
forall {a} (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.
IsList bs =>
(IsList ((a1 : a2 : as) ++ bs) => r) -> r
withIsList2 @bs IsList ((a1 : a2 : as) ++ bs) => r
r = forall (as :: [k]) (bs :: [k]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
(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.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
(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} (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} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[a1, b] @[b, a1] (forall k (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (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} (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} (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** ((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} (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} (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** (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} (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} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[b, a1] @[a1, b] (forall k (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (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} (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 (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} (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} (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (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} (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} (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** ((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 :: [k]). (Monoidal k, Ob as) => Obj (Fold as)
fold :: forall {k} (as :: [k]). (Monoidal k, Ob as) => Obj (Fold as)
fold = forall (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @as Unit ~> Unit
Fold as ~> Fold as
(as ~ '[]) => Fold as ~> Fold as
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one Obj a
Fold as ~> Fold as
forall (a :: k). (Ob a, as ~ '[a]) => Fold as ~> Fold as
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj \ @b @bs -> forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b
-> (Fold (c : cs) ~> Fold (c : cs))
-> (b ** Fold (c : cs)) ~> (b ** Fold (c : cs))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (as :: [k]). (Monoidal k, Ob as) => Obj (Fold as)
forall {k} (as :: [k]). (Monoidal k, Ob as) => Obj (Fold as)
fold @bs

withObFold :: forall {k} (as :: [k]) r. (Monoidal k, Ob as) => ((Ob (Fold as)) => r) -> r
withObFold :: forall {k} (as :: [k]) r.
(Monoidal k, Ob as) =>
(Ob (Fold as) => r) -> r
withObFold Ob (Fold as) => r
r = forall (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @as r
(as ~ '[]) => r
Ob (Fold as) => r
r r
Ob (Fold as) => r
forall (a :: k). (Ob a, as ~ '[a]) => r
r \ @b @bs -> forall (as :: [k]) r.
(Monoidal k, Ob as) =>
(Ob (Fold as) => r) -> r
forall {k} (as :: [k]) r.
(Monoidal k, Ob as) =>
(Ob (Fold as) => r) -> r
withObFold @bs ((Ob (Fold bs) => r) -> r) -> (Ob (Fold bs) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @b @(Fold bs) r
Ob (b ** Fold bs) => r
Ob (Fold as) => r
r

type family Obs (as :: [k]) :: Constraint where
  Obs '[] = ()
  Obs (a ': as) = (Ob a, Obs as)

withObs :: forall {k} (as :: [k]) r. (Monoidal k, Ob as) => ((Obs as) => r) -> r
withObs :: forall {k} (as :: [k]) r. (Monoidal k, Ob as) => (Obs as => r) -> r
withObs Obs as => r
r = forall (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @as r
(as ~ '[]) => r
Obs as => r
r r
Obs as => r
forall (a :: k). (Ob a, as ~ '[a]) => r
r \ @_ @bs -> forall (as :: [k]) r. (Monoidal k, Ob as) => (Obs as => r) -> r
forall {k} (as :: [k]) r. (Monoidal k, Ob as) => (Obs as => r) -> r
withObs @bs r
Obs as => r
Obs bs => r
r

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 :: Obj (Fold bs)
fbs = forall (as :: [k]). (Monoidal k, Ob as) => Obj (Fold as)
forall {k} (as :: [k]). (Monoidal k, Ob as) => Obj (Fold as)
fold @bs
      h :: forall (cs :: [k]) r. (Ob cs) => ((Ob (Fold cs)) => Fold cs ** Fold bs ~> Fold (cs ++ bs) -> r) -> r
      h :: forall (cs :: [k]) r.
Ob cs =>
(Ob (Fold cs) => ((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r)
-> r
h Ob (Fold cs) => ((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r
k =
        forall (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @cs
          (Ob (Fold cs) => ((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r
((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r
k (Unit ** Fold bs) ~> Fold bs
(Fold cs ** Fold bs) ~> Fold (cs ++ bs)
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor)
          (\ @c -> Ob (Fold cs) => ((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r
((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r
k (((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r)
-> ((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r
forall a b. (a -> b) -> a -> b
$ forall (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @bs (a ** Unit) ~> a
(Fold cs ** Fold bs) ~> Fold (cs ++ bs)
(bs ~ '[]) => (Fold cs ** Fold bs) ~> Fold (cs ++ bs)
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** a ~> a
Obj (Fold bs)
fbs) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj a
-> ((b ** Fold (c : cs)) ~> (b ** Fold (c : cs)))
-> (a ** (b ** Fold (c : cs))) ~> (a ** (b ** Fold (c : cs)))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** (b ** Fold (c : cs)) ~> (b ** Fold (c : cs))
Obj (Fold bs)
fbs))
          (\ @c @cs' -> forall (cs :: [k]) r.
Ob cs =>
(Ob (Fold cs) => ((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r)
-> r
h @cs' \(Fold bs ** Fold bs) ~> Fold (bs ++ bs)
cbs -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @c @(Fold cs') ((Ob (b ** Fold bs) => r) -> r) -> (Ob (b ** Fold bs) => r) -> r
forall a b. (a -> b) -> a -> b
$ Ob (Fold cs) => ((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r
((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r
k (((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r)
-> ((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj b
-> ((Fold (c : cs) ** Fold bs) ~> Fold (c : (cs ++ bs)))
-> (b ** (Fold (c : cs) ** Fold bs))
   ~> (b ** Fold (c : (cs ++ bs)))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** (Fold bs ** Fold bs) ~> Fold (bs ++ bs)
(Fold (c : cs) ** Fold bs) ~> Fold (c : (cs ++ bs))
cbs) ((b ** (Fold (c : cs) ** Fold bs)) ~> Fold (cs ++ bs))
-> ((Fold cs ** Fold bs) ~> (b ** (Fold (c : cs) ** Fold bs)))
-> (Fold cs ** Fold bs) ~> Fold (cs ++ bs)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @c @(Fold cs') @(Fold bs))
          ((Ob (Fold bs), Ob (Fold bs)) => r) -> Obj (Fold bs) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Obj (Fold bs)
fbs
  in forall (cs :: [k]) r.
Ob cs =>
(Ob (Fold cs) => ((Fold cs ** Fold bs) ~> Fold (cs ++ bs)) -> r)
-> r
h @as Ob (Fold as) =>
((Fold as ** Fold bs) ~> Fold (as ++ bs))
-> (Fold as ** Fold bs) ~> Fold (as ++ bs)
((Fold as ** Fold bs) ~> Fold (as ++ bs))
-> (Fold as ** Fold bs) ~> Fold (as ++ bs)
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

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 :: Obj (Fold bs)
fbs = forall (as :: [k]). (Monoidal k, Ob as) => Obj (Fold as)
forall {k} (as :: [k]). (Monoidal k, Ob as) => Obj (Fold as)
fold @bs
      h :: forall (cs :: [k]) r. (Ob cs) => ((Ob (Fold cs)) => Fold (cs ++ bs) ~> Fold cs ** Fold bs -> r) -> r
      h :: forall (cs :: [k]) r.
Ob cs =>
(Ob (Fold cs) => (Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r)
-> r
h Ob (Fold cs) => (Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r
k =
        forall (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @cs
          (Ob (Fold cs) => (Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r
(Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r
k Fold bs ~> (Unit ** Fold bs)
Fold (cs ++ bs) ~> (Fold cs ** Fold bs)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv)
          (\ @c -> Ob (Fold cs) => (Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r
(Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r
k ((Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r)
-> (Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r
forall a b. (a -> b) -> a -> b
$ forall (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
forall {k} (as :: [k]) r.
IsList as =>
((as ~ '[]) => r)
-> (forall (a :: k). (Ob a, as ~ '[a]) => r)
-> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]).
    (Ob b, Ob bs, Ob cs, as ~ (b : bs), bs ~ (c : cs)) =>
    r)
-> r
listCase @bs a ~> (a ** Unit)
Fold (cs ++ bs) ~> (Fold cs ** Fold bs)
(bs ~ '[]) => Fold (cs ++ bs) ~> (Fold cs ** Fold bs)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** a ~> a
Obj (Fold bs)
fbs) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj a
-> ((b ** Fold (c : cs)) ~> (b ** Fold (c : cs)))
-> (a ** (b ** Fold (c : cs))) ~> (a ** (b ** Fold (c : cs)))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** (b ** Fold (c : cs)) ~> (b ** Fold (c : cs))
Obj (Fold bs)
fbs))
          (\ @c @cs' -> forall (cs :: [k]) r.
Ob cs =>
(Ob (Fold cs) => (Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r)
-> r
h @cs' \Fold (bs ++ bs) ~> (Fold bs ** Fold bs)
cbs -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @c @(Fold cs') ((Ob (b ** Fold bs) => r) -> r) -> (Ob (b ** Fold bs) => r) -> r
forall a b. (a -> b) -> a -> b
$ Ob (Fold cs) => (Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r
(Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r
k ((Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r)
-> (Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @c @(Fold cs') @(Fold bs) ((b ** (Fold (c : cs) ** Fold bs)) ~> (Fold cs ** Fold bs))
-> (Fold (cs ++ bs) ~> (b ** (Fold (c : cs) ** Fold bs)))
-> Fold (cs ++ bs) ~> (Fold cs ** Fold bs)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (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} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj b
-> (Fold (c : (cs ++ bs)) ~> (Fold (c : cs) ** Fold bs))
-> (b ** Fold (c : (cs ++ bs)))
   ~> (b ** (Fold (c : cs) ** Fold bs))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** Fold (c : (cs ++ bs)) ~> (Fold (c : cs) ** Fold bs)
Fold (bs ++ bs) ~> (Fold bs ** Fold bs)
cbs))
          ((Ob (Fold bs), Ob (Fold bs)) => r) -> Obj (Fold bs) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Obj (Fold bs)
fbs
  in forall (cs :: [k]) r.
Ob cs =>
(Ob (Fold cs) => (Fold (cs ++ bs) ~> (Fold cs ** Fold bs)) -> r)
-> r
h @as Ob (Fold as) =>
(Fold (as ++ bs) ~> (Fold as ** Fold bs))
-> Fold (as ++ bs) ~> (Fold as ** Fold bs)
(Fold (as ++ bs) ~> (Fold as ** Fold bs))
-> Fold (as ++ bs) ~> (Fold as ** Fold bs)
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

type Strictified :: CAT [k]
data Strictified as bs where
  Str :: (Ob as, Ob bs) => {forall {k} (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 (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> '[a] ~> '[b]
singleton a ~> b
a = (Fold '[a] ~> Fold '[b]) -> Strictified '[a] '[b]
forall {k} (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. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
a

obj1 :: forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 :: forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 = forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @'[a]

concatMany :: forall {k} (as :: [k]). (Ob as, Monoidal k) => as ~> '[Fold as]
concatMany :: forall {k} (as :: [k]). (Ob as, Monoidal k) => as ~> '[Fold as]
concatMany = forall (as :: [k]) r.
(Monoidal k, Ob as) =>
(Ob (Fold as) => r) -> r
forall {k} (as :: [k]) r.
(Monoidal k, Ob as) =>
(Ob (Fold as) => r) -> r
withObFold @as ((Fold as ~> Fold '[Fold as]) -> Strictified as '[Fold as]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str Fold as ~> Fold as
Fold as ~> Fold '[Fold as]
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

splitMany :: forall {k} (as :: [k]). (Ob as, Monoidal k) => '[Fold as] ~> as
splitMany :: forall {k} (as :: [k]). (Ob as, Monoidal k) => '[Fold as] ~> as
splitMany = forall (as :: [k]) r.
(Monoidal k, Ob as) =>
(Ob (Fold as) => r) -> r
forall {k} (as :: [k]) r.
(Monoidal k, Ob as) =>
(Ob (Fold as) => r) -> r
withObFold @as ((Fold '[Fold as] ~> Fold as) -> Strictified '[Fold as] as
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str Fold as ~> Fold as
Fold '[Fold as] ~> Fold as
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

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 :: 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{} = r
(Ob a, Ob b) => r
r

instance (Monoidal k) => Promonad (Strictified :: CAT [k]) where
  id :: forall (a :: [k]). Ob a => Strictified a a
id @as = (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 (forall (as :: [k]). (Monoidal k, Ob as) => Obj (Fold as)
forall {k} (as :: [k]). (Monoidal k, Ob as) => Obj (Fold as)
fold @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 :: 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
  one :: Strictified Unit Unit
one = Strictified '[] '[]
Strictified Unit Unit
forall (a :: [k]). Ob a => Strictified a a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  Str @as @bs Fold x1 ~> Fold x2
f ** :: forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (x1 ** y1) (x2 ** y2)
** Str @cs @ds Fold y1 ~> Fold y2
g =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @[k] @as @cs ((Ob (x1 ** y1) => Strictified (x1 ** y1) (x2 ** y2))
 -> Strictified (x1 ** y1) (x2 ** y2))
-> (Ob (x1 ** y1) => Strictified (x1 ** y1) (x2 ** y2))
-> Strictified (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @[k] @bs @ds ((Ob (x2 ** y2) => Strictified (x1 ** y1) (x2 ** y2))
 -> Strictified (x1 ** y1) (x2 ** y2))
-> (Ob (x2 ** y2) => Strictified (x1 ** y1) (x2 ** y2))
-> Strictified (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
        (Fold (x1 ++ y1) ~> Fold (x2 ++ y2))
-> Strictified (x1 ++ y1) (x2 ++ y2)
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 x2 ** Fold y2) ~> Fold (x2 ++ y2))
-> (Fold (x1 ++ y1) ~> (Fold x2 ** Fold y2))
-> Fold (x1 ++ y1) ~> Fold (x2 ++ y2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Fold x1 ~> Fold x2
f (Fold x1 ~> Fold x2)
-> (Fold y1 ~> Fold y2)
-> (Fold x1 ** Fold y1) ~> (Fold x2 ** Fold y2)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** Fold y1 ~> Fold y2
g) ((Fold x1 ** Fold y1) ~> (Fold x2 ** Fold y2))
-> (Fold (x1 ++ y1) ~> (Fold x1 ** Fold y1))
-> Fold (x1 ++ y1) ~> (Fold x2 ** Fold y2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (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} (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.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @as @bs Ob (a ** b) => r
r = forall (as :: [k]) (bs :: [k]) r.
(IsList as, IsList bs) =>
(IsList (as ++ bs) => r) -> r
forall {k} (as :: [k]) (bs :: [k]) r.
(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} (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} (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} (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} (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} (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (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} (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (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} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: [k]). (CategoryOf [k], Ob a) => Obj a
forall {k} (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} (as :: [k]) (bs :: [k]).
(IsList as, IsList bs, SymMonoidal k) =>
(as ++ bs) ~> (bs ++ as)
swap' @as @bs

swap2 :: forall {k} (a :: k) (b :: k). (SymMonoidal k, Ob a, Ob b) => '[a, b] ~> '[b, a]
swap2 :: forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
'[a, b] ~> '[b, a]
swap2 = forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @[k] @'[a] @'[b]