{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Hypergraph where

import Data.Type.Nat (Nat (..), SNat (..), SNatI, snat)
import Prelude (($))

import Proarrow.Category (Supplies)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), (==))
import Proarrow.Category.Monoidal.CompactClosed (CompactClosed)
import Proarrow.Category.Monoidal.Strictified (Strictified (..), obj1, singleton, swap2)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj)
import Proarrow.Monoid (Comonoid (..), Monoid (..), comultS, mappendS)

type family NFold (n :: Nat) (x :: k) :: k where
  NFold Z x = Unit
  NFold (S n) x = x ** NFold n x

type family NFoldS (n :: Nat) (x :: k) :: [k] where
  NFoldS Z x = '[]
  NFoldS (S n) x = x ': NFoldS n x

withObNFold :: forall {k} n (a :: k) r. (SNatI n, Ob a, Monoidal k) => ((Ob (NFold n a)) => r) -> r
withObNFold :: forall {k} (n :: Nat) (a :: k) r.
(SNatI n, Ob a, Monoidal k) =>
(Ob (NFold n a) => r) -> r
withObNFold Ob (NFold n a) => r
r = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> r
Ob (NFold n a) => r
r
  SS @n' -> forall {k} (n :: Nat) (a :: k) r.
(SNatI n, Ob a, Monoidal k) =>
(Ob (NFold n a) => r) -> r
forall (n :: Nat) (a :: k) r.
(SNatI n, Ob a, Monoidal k) =>
(Ob (NFold n a) => r) -> r
withObNFold @n' @a (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @(NFold n' a) r
Ob (a ** NFold n1 a) => r
Ob (NFold n a) => r
r)

fanIn :: forall n a. (SNatI n, Monoid a) => NFold n a ~> a
fanIn :: forall {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFold n a ~> a
fanIn = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> Unit ~> a
NFold n a ~> a
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  SS @n' -> forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a ((a ** a) ~> a)
-> ((a ** NFold n1 a) ~> (a ** a)) -> (a ** NFold n1 a) ~> a
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 @a Obj a -> (NFold n1 a ~> a) -> (a ** NFold n1 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)
** forall {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFold n a ~> a
forall (n :: Nat) (a :: k). (SNatI n, Monoid a) => NFold n a ~> a
fanIn @n' @a)

fanInS :: forall n a. (SNatI n, Monoid a) => NFoldS n a ~> '[a]
fanInS :: forall {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFoldS n a ~> '[a]
fanInS =
  case forall (n :: Nat). SNatI n => SNat n
snat @n of
    SNat n
SZ -> (Fold '[] ~> Fold '[a]) -> Strictified '[] '[a]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str Unit ~> a
Fold '[] ~> Fold '[a]
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
    SS @n' -> forall (m :: k). Monoid m => '[m, m] ~> '[m]
forall {k} (m :: k). Monoid m => '[m, m] ~> '[m]
mappendS @a Strictified '[a, a] '[a]
-> Strictified (a : NFoldS n1 a) '[a, a]
-> Strictified (a : NFoldS n1 a) '[a]
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). (Monoidal k, Ob a) => Obj '[a]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 @a Strictified '[a] '[a]
-> Strictified (NFoldS n1 a) '[a]
-> Strictified ('[a] ** NFoldS n1 a) ('[a] ** '[a])
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 {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFoldS n a ~> '[a]
forall (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFoldS n a ~> '[a]
fanInS @n' @a)

fanOut :: forall n a. (SNatI n, Comonoid a) => a ~> NFold n a
fanOut :: forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
a ~> NFold n a
fanOut = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> a ~> Unit
a ~> NFold n a
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  SS @n' -> (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> NFold n1 a) -> (a ** a) ~> (a ** NFold n1 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)
** forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
a ~> NFold n a
forall (n :: Nat) (a :: k). (SNatI n, Comonoid a) => a ~> NFold n a
fanOut @n' @a) ((a ** a) ~> (a ** NFold n1 a))
-> (a ~> (a ** a)) -> a ~> (a ** NFold n1 a)
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 (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a

fanOutS :: forall n a. (SNatI n, Comonoid a) => '[a] ~> NFoldS n a
fanOutS :: forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
'[a] ~> NFoldS n a
fanOutS =
  case forall (n :: Nat). SNatI n => SNat n
snat @n of
    SNat n
SZ -> (Fold '[a] ~> Fold '[]) -> Strictified '[a] '[]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str a ~> Unit
Fold '[a] ~> Fold '[]
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
    SS @n' -> (forall (a :: k). (Monoidal k, Ob a) => Obj '[a]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 @a Strictified '[a] '[a]
-> Strictified '[a] (NFoldS n1 a)
-> Strictified ('[a] ** '[a]) ('[a] ** NFoldS n1 a)
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 {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
'[a] ~> NFoldS n a
forall (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
'[a] ~> NFoldS n a
fanOutS @n' @a) Strictified ('[a] ++ '[a]) (a : NFoldS n1 a)
-> Strictified '[a] ('[a] ++ '[a])
-> Strictified '[a] (a : NFoldS n1 a)
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 (c :: k). Comonoid c => '[c] ~> '[c, c]
forall {k} (c :: k). Comonoid c => '[c] ~> '[c, c]
comultS @a

-- | We have a special frobenius algebra for an object if it is a monoid and a comonoid in a nice compatible way.
-- Then there's a unique way to go from n-fold @a@ to m-fold @a@.
class (Monoid a, Comonoid a) => Frobenius a

spider :: forall n m a. (Frobenius a, SNatI n, SNatI m) => NFold n a ~> NFold m a
spider :: forall {k} (n :: Nat) (m :: Nat) (a :: k).
(Frobenius a, SNatI n, SNatI m) =>
NFold n a ~> NFold m a
spider = forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
a ~> NFold n a
forall (n :: Nat) (a :: k). (SNatI n, Comonoid a) => a ~> NFold n a
fanOut @m @a (a ~> NFold m a) -> (NFold n a ~> a) -> NFold n a ~> NFold m a
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} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFold n a ~> a
forall (n :: Nat) (a :: k). (SNatI n, Monoid a) => NFold n a ~> a
fanIn @n @a

spiderS :: forall n m a. (Frobenius a, SNatI n, SNatI m) => NFoldS n a ~> NFoldS m a
spiderS :: forall {k} (n :: Nat) (m :: Nat) (a :: k).
(Frobenius a, SNatI n, SNatI m) =>
NFoldS n a ~> NFoldS m a
spiderS = forall {k} (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
'[a] ~> NFoldS n a
forall (n :: Nat) (a :: k).
(SNatI n, Comonoid a) =>
'[a] ~> NFoldS n a
fanOutS @m @a Strictified '[a] (NFoldS m a)
-> Strictified (NFoldS n a) '[a]
-> Strictified (NFoldS n a) (NFoldS m a)
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 {k} (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFoldS n a ~> '[a]
forall (n :: Nat) (a :: k).
(SNatI n, Monoid a) =>
NFoldS n a ~> '[a]
fanInS @n @a

cup :: (Frobenius a) => Unit ~> a ** a
cup :: forall {k} (a :: k). Frobenius a => Unit ~> (a ** a)
cup @a = forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @a (a ~> (a ** a)) -> (Unit ~> a) -> Unit ~> (a ** a)
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 (m :: k). Monoid m => Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty @a

cupS :: (Frobenius a) => '[] ~> [a, a]
cupS :: forall {a} (a :: a). Frobenius a => '[] ~> '[a, a]
cupS @a = (Fold '[] ~> Fold '[a, a]) -> Strictified '[] '[a, a]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall (a :: a). Frobenius a => Unit ~> (a ** a)
forall {k} (a :: k). Frobenius a => Unit ~> (a ** a)
cup @a)

cap :: (Frobenius a) => a ** a ~> Unit
cap :: forall {k} (a :: k). Frobenius a => (a ** a) ~> Unit
cap @a = forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @a (a ~> Unit) -> ((a ** a) ~> a) -> (a ** a) ~> Unit
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 (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @a

capS :: (Frobenius a) => [a, a] ~> '[]
capS :: forall {k} (a :: k). Frobenius a => '[a, a] ~> '[]
capS @a = (Fold '[a, a] ~> Fold '[]) -> Strictified '[a, a] '[]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall (a :: k). Frobenius a => (a ** a) ~> Unit
forall {k} (a :: k). Frobenius a => (a ** a) ~> Unit
cap @a)

-- | A hypergraph category has a special frobenius algebra for every object, and the
-- frobenius algebra of any tensor product X ⊗ Y is induced in the canonical way from those of X and Y.
class (k `Supplies` Frobenius, CompactClosed k) => Hypergraph k

-- | A hypergraph category is self-dual compact closed.
dualHG :: forall {k} (a :: k) b. (Hypergraph k) => a ~> b -> b ~> a
dualHG :: forall {k} (a :: k) (b :: k). Hypergraph k => (a ~> b) -> b ~> a
dualHG a ~> b
f =
  forall (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr @'[b] @'[a] (Strictified '[b] '[a] -> Fold '[b] ~> Fold '[a])
-> Strictified '[b] '[a] -> Fold '[b] ~> Fold '[a]
forall a b. (a -> b) -> a -> b
$
    '[] ~> '[a, a]
Strictified '[] '[a, a]
forall {a} (a :: a). Frobenius a => '[] ~> '[a, a]
cupS Strictified '[] '[a, a]
-> Strictified '[b] '[b]
-> Strictified ('[] ** '[b]) ('[a, 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)
** Obj '[b]
Strictified '[b] '[b]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
      ('[b] ~> ('[a, a] ++ '[b]))
-> (('[a, a] ++ '[b]) ~> (('[a] ++ '[b]) ++ '[b]))
-> '[b] ~> (('[a] ++ '[b]) ++ '[b])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== Obj '[a]
Strictified '[a] '[a]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Strictified '[a] '[a]
-> Strictified '[a] '[b]
-> Strictified ('[a] ** '[a]) ('[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)
** (a ~> b) -> '[a] ~> '[b]
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> '[a] ~> '[b]
singleton a ~> b
f Strictified ('[a] ++ '[a]) ('[a] ++ '[b])
-> Strictified '[b] '[b]
-> Strictified (('[a] ++ '[a]) ** '[b]) (('[a] ++ '[b]) ** '[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)
** Obj '[b]
Strictified '[b] '[b]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
      ('[b] ~> (('[a] ++ '[b]) ++ '[b]))
-> ((('[a] ++ '[b]) ++ '[b]) ~> '[a]) -> '[b] ~> '[a]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== Obj '[a]
Strictified '[a] '[a]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Strictified '[a] '[a]
-> Strictified '[b, b] '[]
-> Strictified ('[a] ** '[b, b]) ('[a] ** '[])
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, b] ~> '[]
Strictified '[b, b] '[]
forall {k} (a :: k). Frobenius a => '[a, a] ~> '[]
capS
      ((Ob a, Ob b) => Strictified '[b] '[a])
-> (a ~> b) -> Strictified '[b] '[a]
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
f

linDistHG :: forall {k} (a :: k) b c. (Hypergraph k, Ob a, Ob b) => a ** b ~> c -> a ~> b ** c
linDistHG :: forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ** c)
linDistHG (a ** b) ~> c
f =
  forall (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr @'[a] @[b, c] (Strictified '[a] '[b, c] -> Fold '[a] ~> Fold '[b, c])
-> Strictified '[a] '[b, c] -> Fold '[a] ~> Fold '[b, c]
forall a b. (a -> b) -> a -> b
$
    Obj '[a]
Strictified '[a] '[a]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Strictified '[a] '[a]
-> Strictified '[] '[b, b]
-> Strictified ('[a] ** '[]) ('[a] ** '[b, 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, b]
Strictified '[] '[b, b]
forall {a} (a :: a). Frobenius a => '[] ~> '[a, a]
cupS
      ('[a] ~> ('[a] ++ '[b, b]))
-> (('[a] ++ '[b, b]) ~> '[c, b]) -> '[a] ~> '[c, b]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> 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 @[a, b] @'[c] (a ** b) ~> c
Fold '[a, b] ~> Fold '[c]
f Strictified '[a, b] '[c]
-> Strictified '[b] '[b]
-> Strictified ('[a, b] ** '[b]) ('[c] ** '[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)
** Obj '[b]
Strictified '[b] '[b]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
      ('[a] ~> '[c, b]) -> ('[c, b] ~> '[b, c]) -> '[a] ~> '[b, c]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== '[c, b] ~> '[b, c]
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
'[a, b] ~> '[b, a]
swap2
      ((Ob (a ** b), Ob c) => Strictified '[a] '[b, c])
-> ((a ** b) ~> c) -> Strictified '[a] '[b, c]
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) ~> c
f

linDistInvHG :: forall {k} (a :: k) b c. (Hypergraph k, Ob b, Ob c) => a ~> b ** c -> a ** b ~> c
linDistInvHG :: forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob b, Ob c) =>
(a ~> (b ** c)) -> (a ** b) ~> c
linDistInvHG a ~> (b ** c)
f =
  forall (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr @[a, b] @'[c] (Strictified '[a, b] '[c] -> Fold '[a, b] ~> Fold '[c])
-> Strictified '[a, b] '[c] -> Fold '[a, b] ~> Fold '[c]
forall a b. (a -> b) -> a -> b
$
    '[a, b] ~> '[b, a]
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
'[a, b] ~> '[b, a]
swap2
      ('[a, b] ~> '[b, a])
-> ('[b, a] ~> ('[b] ++ '[b, c])) -> '[a, b] ~> ('[b] ++ '[b, c])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== Obj '[b]
Strictified '[b] '[b]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Strictified '[b] '[b]
-> Strictified '[a] '[b, c]
-> Strictified ('[b] ** '[a]) ('[b] ** '[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 (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 @'[a] @[b, c] a ~> (b ** c)
Fold '[a] ~> Fold '[b, c]
f
      ('[a, b] ~> ('[b] ++ '[b, c]))
-> (('[b] ++ '[b, c]) ~> '[c]) -> '[a, b] ~> '[c]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== '[b, b] ~> '[]
Strictified '[b, b] '[]
forall {k} (a :: k). Frobenius a => '[a, a] ~> '[]
capS Strictified '[b, b] '[]
-> Strictified '[c] '[c]
-> Strictified ('[b, b] ** '[c]) ('[] ** '[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)
** Obj '[c]
Strictified '[c] '[c]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
      ((Ob a, Ob (b ** c)) => Strictified '[a, b] '[c])
-> (a ~> (b ** c)) -> Strictified '[a, b] '[c]
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 ** c)
f

-- | A hypergraph category has a trace.
traceHG :: forall {k} u (x :: k) y. (Hypergraph k, Ob x, Ob y, Ob u) => u ** x ~> u ** y -> x ~> y
traceHG :: forall {k} (u :: k) (x :: k) (y :: k).
(Hypergraph k, Ob x, Ob y, Ob u) =>
((u ** x) ~> (u ** y)) -> x ~> y
traceHG (u ** x) ~> (u ** y)
f =
  Strictified '[x] '[y] -> Fold '[x] ~> Fold '[y]
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr (Strictified '[x] '[y] -> Fold '[x] ~> Fold '[y])
-> Strictified '[x] '[y] -> Fold '[x] ~> Fold '[y]
forall a b. (a -> b) -> a -> b
$
    '[] ~> '[u, u]
forall {a} (a :: a). Frobenius a => '[] ~> '[a, a]
cupS ('[] ~> '[u, u])
-> ('[x] ~> '[x]) -> ('[] ** '[x]) ~> ('[u, u] ** '[x])
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)
** '[x] ~> '[x]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1
      (('[] ** '[x]) ~> ('[u, u] ** '[x]))
-> (('[u, u] ** '[x]) ~> ('[u] ++ '[u, y]))
-> ('[] ** '[x]) ~> ('[u] ++ '[u, y])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== Obj '[u]
Strictified '[u] '[u]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Strictified '[u] '[u]
-> Strictified '[u, x] '[u, y]
-> Strictified ('[u] ** '[u, x]) ('[u] ** '[u, y])
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 (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 @[u, x] @'[u, y] (u ** x) ~> (u ** y)
Fold '[u, x] ~> Fold '[u, y]
f
      (('[] ** '[x]) ~> ('[u] ++ '[u, y]))
-> (('[u] ++ '[u, y]) ~> ('[] ++ '[y]))
-> ('[] ** '[x]) ~> ('[] ++ '[y])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== '[u, u] ~> '[]
Strictified '[u, u] '[]
forall {k} (a :: k). Frobenius a => '[a, a] ~> '[]
capS Strictified '[u, u] '[]
-> Strictified '[y] '[y]
-> Strictified ('[u, u] ** '[y]) ('[] ** '[y])
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)
** Obj '[y]
Strictified '[y] '[y]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1

-- | A hypergraph category is monoidal closed.
type ExpHG a b = a ** b

curryHG :: forall {k} (a :: k) b c. (Hypergraph k, Ob a, Ob b) => a ** b ~> c -> a ~> ExpHG b c
curryHG :: forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ** c)
curryHG = forall (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ** c)
forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ** c)
linDistHG @a @b @c

applyHG :: forall {k} (b :: k) c. (Hypergraph k, Ob b, Ob c) => ExpHG b c ** b ~> c
applyHG :: forall {k} (b :: k) (c :: k).
(Hypergraph k, Ob b, Ob c) =>
(ExpHG b c ** b) ~> c
applyHG = forall (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob b, Ob c) =>
(a ~> (b ** c)) -> (a ** b) ~> c
forall {k} (a :: k) (b :: k) (c :: k).
(Hypergraph k, Ob b, Ob c) =>
(a ~> (b ** c)) -> (a ** b) ~> c
linDistInvHG @_ @b (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> (c ~> c) -> (b ** c) ~> (b ** c)
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 (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c)