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

module Proarrow.Profunctor.PastroTambara where

import Prelude (($))

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (Monoidal (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..), composeActs, decomposeActs)
import Proarrow.Category.Monoidal.Optic (ExOptic (..))
import Proarrow.Category.Opposite (OPPOSITE (..))
import Proarrow.Core (CategoryOf (..), Kind, Profunctor (..), Promonad (..), obj, (//), (:~>), type (+->), src, tgt, OB)
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Costar (Costar, pattern Costar)
import Proarrow.Profunctor.Star (Star, pattern Star)
import Proarrow.Profunctor.Yoneda (Yo (..))
import Proarrow.Profunctor.Free (HasFree (..))
import Proarrow.Profunctor.Cofree (HasCofree (..))

type Pastro :: Kind -> j +-> k -> j +-> k
data Pastro m p a b where
  Pastro :: forall {m} (z :: m) x y p a b. (Ob z) => a ~> Act z x -> p x y -> Act z y ~> b -> Pastro m p a b

pastro :: forall {j} {k} m (p :: j +-> k). (Profunctor p, MonoidalAction m j, MonoidalAction m k) => p :~> Pastro m p
pastro :: forall {j} {k} m (p :: j +-> k).
(Profunctor p, MonoidalAction m j, MonoidalAction m k) =>
p :~> Pastro m p
pastro p a b
p = forall (z :: m) (x :: k) (y :: j) (p :: j +-> k) (a :: k) (b :: j).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
forall {k} {k} {m} (z :: m) (x :: k) (y :: k) (p :: k +-> k)
       (a :: k) (b :: k).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
Pastro @Unit (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m) p a b
p (forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m) ((Ob a, Ob b) => Pastro m p a b) -> p a b -> Pastro m p a b
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

unpastro :: forall {j} {k} m (p :: j +-> k). (Strong m p, MonoidalAction m j, MonoidalAction m k) => Pastro m p :~> p
unpastro :: forall {j} {k} m (p :: j +-> k).
(Strong m p, MonoidalAction m j, MonoidalAction m k) =>
Pastro m p :~> p
unpastro (Pastro @z a ~> Act z x
f p x y
p Act z y ~> b
g) = (a ~> Act z x) -> (Act z y ~> b) -> p (Act z x) (Act z y) -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> Act z x
f Act z y ~> b
g ((z ~> z) -> p x y -> p (Act z x) (Act z y)
forall (a :: m) (b :: m) (x :: k) (y :: j).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @z) p x y
p)

instance (CategoryOf j, CategoryOf k) => Profunctor (Pastro m p :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Pastro m p a b -> Pastro m p c d
dimap c ~> a
l b ~> d
r (Pastro @z a ~> Act z x
f p x y
p Act z y ~> b
g) = forall (z :: m) (x :: k) (y :: j) (p :: j +-> k) (a :: k) (b :: j).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
forall {k} {k} {m} (z :: m) (x :: k) (y :: k) (p :: k +-> k)
       (a :: k) (b :: k).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
Pastro @z (a ~> Act z x
f (a ~> Act z x) -> (c ~> a) -> c ~> Act z x
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
. c ~> a
l) p x y
p (b ~> d
r (b ~> d) -> (Act z y ~> b) -> Act z y ~> d
forall (b :: j) (c :: j) (a :: j). (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
. Act z y ~> b
g)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Pastro m p a b -> r
\\ Pastro a ~> Act z x
f p x y
_ Act z y ~> b
g = r
(Ob a, Ob b) => r
(Ob a, Ob (Act z x)) => r
r ((Ob a, Ob (Act z x)) => r) -> (a ~> Act z x) -> 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
\\ a ~> Act z x
f ((Ob (Act z y), Ob b) => r) -> (Act z y ~> b) -> r
forall (a :: j) (b :: j) 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
\\ Act z y ~> b
g
instance (MonoidalAction m j, MonoidalAction m k, Profunctor p) => Strong m (Pastro m p :: j +-> k) where
  act :: forall (a :: m) (b :: m) (x :: k) (y :: j).
(a ~> b) -> Pastro m p x y -> Pastro m p (Act a x) (Act b y)
act @_ @b @x @y a ~> b
m (Pastro @z @x1 @y1 x ~> Act z x
f p x y
p Act z y ~> y
g) =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @m @b @z
      (forall (z :: m) (x :: k) (y :: j) (p :: j +-> k) (a :: k) (b :: j).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
forall {k} {k} {m} (z :: m) (x :: k) (y :: k) (p :: k +-> k)
       (a :: k) (b :: k).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
Pastro @(b ** z) (forall (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(a ~> Act x b) -> (b ~> Act y c) -> a ~> Act (x ** y) c
forall {m} {k} (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(a ~> Act x b) -> (b ~> Act y c) -> a ~> Act (x ** y) c
composeActs @b @z @x1 (a ~> b
m (a ~> b) -> (x ~> x) -> Act a x ~> Act b x
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x) x ~> Act z x
f) p x y
p (forall (x :: m) (y :: m) (c :: j) (a :: j) (b :: j).
(MonoidalAction m j, Ob x, Ob y, Ob c) =>
(Act y c ~> b) -> (Act x b ~> a) -> Act (x ** y) c ~> a
forall {m} {k} (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(Act y c ~> b) -> (Act x b ~> a) -> Act (x ** y) c ~> a
decomposeActs @b @z @y1 Act z y ~> y
g (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> (y ~> y) -> Act b y ~> Act b y
forall (a :: m) (b :: m) (x :: j) (y :: j).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @y)))
      ((Ob a, Ob b) => Pastro m p (Act a x) (Act b y))
-> (a ~> b) -> Pastro m p (Act a x) (Act b y)
forall (a :: m) (b :: m) 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
m
      ((Ob x, Ob (Act z x)) => Pastro m p (Act a x) (Act b y))
-> (x ~> Act z x) -> Pastro m p (Act a x) (Act b y)
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
\\ x ~> Act z x
f
      ((Ob (Act z y), Ob y) => Pastro m p (Act a x) (Act b y))
-> (Act z y ~> y) -> Pastro m p (Act a x) (Act b y)
forall (a :: j) (b :: j) 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
\\ Act z y ~> y
g
      ((Ob x, Ob y) => Pastro m p (Act a x) (Act b y))
-> p x y -> Pastro m p (Act a x) (Act b y)
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p 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
\\ p x y
p

instance (MonoidalAction m j, MonoidalAction m k) => HasFree (Strong m :: OB (j +-> k)) where
  type Free (Strong m) = Star (Pastro m)
  lift' :: forall (a :: j +-> k) (b :: j +-> k).
(a ~> b) -> Free (Strong m) a b
lift' a ~> b
n = (a ~> Pastro m b) -> Star' ('NT (Pastro m)) a b
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((b :~> Pastro m b) -> Prof b (Pastro m b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof b a b -> Pastro m b a b
b :~> Pastro m b
forall {j} {k} m (p :: j +-> k).
(Profunctor p, MonoidalAction m j, MonoidalAction m k) =>
p :~> Pastro m p
pastro Prof b (Pastro m b) -> Prof a b -> Prof a (Pastro m b)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Prof b c -> Prof a b -> Prof a c
. a ~> b
Prof a b
n) ((Ob a, Ob b) => Star' ('NT (Pastro m)) a b)
-> Prof a b -> Star' ('NT (Pastro m)) a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j +-> k) (b :: j +-> k) r.
((Ob a, Ob b) => r) -> Prof a b -> r
\\ a ~> b
Prof a b
n
  retract' :: forall (b :: j +-> k) (a :: j +-> k).
Strong m b =>
Free (Strong m) a b -> a ~> b
retract' (Star a ~> Pastro m b
n) = (Pastro m b :~> b) -> Prof (Pastro m b) b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof Pastro m b a b -> b a b
Pastro m b :~> b
forall {j} {k} m (p :: j +-> k).
(Strong m p, MonoidalAction m j, MonoidalAction m k) =>
Pastro m p :~> p
unpastro  Prof (Pastro m b) b -> Prof a (Pastro m b) -> Prof a b
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Prof b c -> Prof a b -> Prof a c
. a ~> Pastro m b
Prof a (Pastro m b)
n

instance Functor (Pastro m) where
  map :: forall (a :: k -> j -> Type) (b :: k -> j -> Type).
(a ~> b) -> Pastro m a ~> Pastro m b
map (Prof a :~> b
n) = (Pastro m a :~> Pastro m b) -> Prof (Pastro m a) (Pastro m b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Pastro @z a ~> Act z x
f a x y
p Act z y ~> b
g) -> forall (z :: m) (x :: k) (y :: j) (p :: k -> j -> Type) (a :: k)
       (b :: j).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
forall {k} {k} {m} (z :: m) (x :: k) (y :: k) (p :: k +-> k)
       (a :: k) (b :: k).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
Pastro @z a ~> Act z x
f (a x y -> b x y
a :~> b
n a x y
p) Act z y ~> b
g
instance (MonoidalAction m j, MonoidalAction m k) => Promonad (Star (Pastro m) :: (j +-> k) +-> (j +-> k)) where
  id :: forall (a :: j +-> k). Ob a => Star (Pastro m) a a
id = (a ~> Pastro m a) -> Star (Pastro m) a a
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a :~> Pastro m a) -> Prof a (Pastro m a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof a a b -> Pastro m a a b
a :~> Pastro m a
forall {j} {k} m (p :: j +-> k).
(Profunctor p, MonoidalAction m j, MonoidalAction m k) =>
p :~> Pastro m p
pastro)
  Star b ~> Pastro m c
n . :: forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Star (Pastro m) b c -> Star (Pastro m) a b -> Star (Pastro m) a c
. Star a ~> Pastro m b
m = (a ~> Pastro m c) -> Star (Pastro m) a c
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((Pastro m (Pastro m c) :~> Pastro m c)
-> Prof (Pastro m (Pastro m c)) (Pastro m c)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof Pastro m (Pastro m c) a b -> Pastro m c a b
Pastro m (Pastro m c) :~> Pastro m c
forall {j} {k} m (p :: j +-> k).
(Strong m p, MonoidalAction m j, MonoidalAction m k) =>
Pastro m p :~> p
unpastro Prof (Pastro m (Pastro m c)) (Pastro m c)
-> Prof a (Pastro m (Pastro m c)) -> Prof a (Pastro m c)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Prof b c -> Prof a b -> Prof a c
. (b ~> Pastro m c) -> Pastro m b ~> Pastro m (Pastro m c)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: j +-> k) (b :: j +-> k).
(a ~> b) -> Pastro m a ~> Pastro m b
map b ~> Pastro m c
n Prof (Pastro m b) (Pastro m (Pastro m c))
-> Prof a (Pastro m b) -> Prof a (Pastro m (Pastro m c))
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Prof b c -> Prof a b -> Prof a c
. a ~> Pastro m b
Prof a (Pastro m b)
m)

fromExOptic
  :: forall {j} {k} m (a :: k) (b :: j)
   . (MonoidalAction m j, MonoidalAction m k) => ExOptic m a b :~> (Pastro m (Yo a (OP b)) :: j +-> k)
fromExOptic :: forall {j} {k} m (a :: k) (b :: j).
(MonoidalAction m j, MonoidalAction m k) =>
ExOptic m a b :~> Pastro m (Yo a ('OP b))
fromExOptic (ExOptic @x a ~> Act x a
f x ~> x'
w Act x' b ~> b
g) = forall (z :: m) (x :: k) (y :: j) (p :: j +-> k) (a :: k) (b :: j).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
forall {k} {k} {m} (z :: m) (x :: k) (y :: k) (p :: k +-> k)
       (a :: k) (b :: k).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
Pastro @x a ~> Act x a
f ((a ~> a) -> (b ~> b) -> Yo a ('OP b) a b
forall {k} {j} (c :: k) (a :: k) (b1 :: j) (d :: j).
(c ~> a) -> (b1 ~> d) -> Yo a ('OP b1) c d
Yo a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id) (Act x' b ~> b
g (Act x' b ~> b) -> (Act x b ~> Act x' b) -> Act x b ~> b
forall (b :: j) (c :: j) (a :: j). (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
. (x ~> x'
w (x ~> x') -> (b ~> b) -> Act x b ~> Act x' b
forall (a :: m) (b :: m) (x :: j) (y :: j).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)) ((Ob x, Ob x') => Pastro m (Yo a ('OP b)) a b)
-> (x ~> x') -> Pastro m (Yo a ('OP b)) a b
forall (a :: m) (b :: m) 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
\\ x ~> x'
w

type Tambara :: Kind -> j +-> k -> j +-> k
data Tambara m p a b where
  Tambara :: (Ob a, Ob b) => (forall (z :: m). (Ob z) => p (Act z a) (Act z b)) -> Tambara m p a b

tambara :: forall {j} {k} m (p :: j +-> k). (Strong m p, MonoidalAction m j, MonoidalAction m k) => p :~> Tambara m p
tambara :: forall {j} {k} m (p :: j +-> k).
(Strong m p, MonoidalAction m j, MonoidalAction m k) =>
p :~> Tambara m p
tambara p a b
p = (forall (z :: m). Ob z => p (Act z a) (Act z b)) -> Tambara m p a b
forall {k} {j} (a :: k) (b :: j) m (p :: j +-> k).
(Ob a, Ob b) =>
(forall (z :: m). Ob z => p (Act z a) (Act z b)) -> Tambara m p a b
Tambara (\ @z -> (z ~> z) -> p a b -> p (Act z a) (Act z b)
forall (a :: m) (b :: m) (x :: k) (y :: j).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @z) p a b
p) ((Ob a, Ob b) => Tambara m p a b) -> p a b -> Tambara m p a b
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

untambara
  :: forall {j} {k} m (p :: j +-> k). (Profunctor p, MonoidalAction m j, MonoidalAction m k) => Tambara m p :~> p
untambara :: forall {j} {k} m (p :: j +-> k).
(Profunctor p, MonoidalAction m j, MonoidalAction m k) =>
Tambara m p :~> p
untambara (Tambara forall (z :: m). Ob z => p (Act z a) (Act z b)
p) = (a ~> Act Unit a)
-> (Act Unit b ~> b) -> p (Act Unit a) (Act Unit b) -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m) (forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m) (forall (z :: m). Ob z => p (Act z a) (Act z b)
p @Unit)

instance (MonoidalAction m j, MonoidalAction m k, Profunctor p) => Profunctor (Tambara m p :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Tambara m p a b -> Tambara m p c d
dimap c ~> a
l b ~> d
r (Tambara forall (z :: m). Ob z => p (Act z a) (Act z b)
p) = (forall (z :: m). Ob z => p (Act z c) (Act z d)) -> Tambara m p c d
forall {k} {j} (a :: k) (b :: j) m (p :: j +-> k).
(Ob a, Ob b) =>
(forall (z :: m). Ob z => p (Act z a) (Act z b)) -> Tambara m p a b
Tambara (\ @z -> (Act z c ~> Act z a)
-> (Act z b ~> Act z d)
-> p (Act z a) (Act z b)
-> p (Act z c) (Act z d)
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @z Obj z -> (c ~> a) -> Act z c ~> Act z a
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` c ~> a
l) (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @z Obj z -> (b ~> d) -> Act z b ~> Act z d
forall (a :: m) (b :: m) (x :: j) (y :: j).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` b ~> d
r) (forall (z :: m). Ob z => p (Act z a) (Act z b)
p @z)) ((Ob c, Ob a) => Tambara m p c d) -> (c ~> a) -> Tambara m p c d
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
\\ c ~> a
l ((Ob b, Ob d) => Tambara m p c d) -> (b ~> d) -> Tambara m p c d
forall (a :: j) (b :: j) 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
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Tambara m p a b -> r
\\ Tambara{} = r
(Ob a, Ob b) => r
r
instance (MonoidalAction m j, MonoidalAction m k, Profunctor p) => Strong m (Tambara m p :: j +-> k) where
  act :: forall (a :: m) (b :: m) (x :: k) (y :: j).
(a ~> b) -> Tambara m p x y -> Tambara m p (Act a x) (Act b y)
act @a @b @x @y a ~> b
m (Tambara forall (z :: m). Ob z => p (Act z x) (Act z y)
p) = a ~> b
m (a ~> b)
-> ((Ob a, Ob b) => Tambara m p (Act a x) (Act b y))
-> Tambara m p (Act a x) (Act b y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
    forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @m @k @a @x ((Ob (Act a x) => Tambara m p (Act a x) (Act b y))
 -> Tambara m p (Act a x) (Act b y))
-> (Ob (Act a x) => Tambara m p (Act a x) (Act b y))
-> Tambara m p (Act a x) (Act b y)
forall a b. (a -> b) -> a -> b
$
      forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @m @j @b @y ((Ob (Act b y) => Tambara m p (Act a x) (Act b y))
 -> Tambara m p (Act a x) (Act b y))
-> (Ob (Act b y) => Tambara m p (Act a x) (Act b y))
-> Tambara m p (Act a x) (Act b y)
forall a b. (a -> b) -> a -> b
$
        (forall (z :: m). Ob z => p (Act z (Act a x)) (Act z (Act b y)))
-> Tambara m p (Act a x) (Act b y)
forall {k} {j} (a :: k) (b :: j) m (p :: j +-> k).
(Ob a, Ob b) =>
(forall (z :: m). Ob z => p (Act z a) (Act z b)) -> Tambara m p a b
Tambara \ @z ->
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @m @z @b
            ((Act z (Act a x) ~> Act (z ** b) x)
-> (Act (z ** b) y ~> Act z (Act b y))
-> p (Act (z ** b) x) (Act (z ** b) y)
-> p (Act z (Act a x)) (Act z (Act b y))
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicatorInv @m @k @z @b @x (Act z (Act b x) ~> Act (z ** b) x)
-> (Act z (Act a x) ~> Act z (Act b x))
-> Act z (Act a x) ~> Act (z ** b) x
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
. (z ~> z)
-> (Act a x ~> Act b x) -> Act z (Act a x) ~> Act z (Act b x)
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @z) ((a ~> b) -> (x ~> x) -> Act a x ~> Act b x
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a ~> b
m (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x))) (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicator @m @j @z @b @y) (forall (z :: m). Ob z => p (Act z x) (Act z y)
p @(z ** b)))

instance (MonoidalAction m j, MonoidalAction m k) => HasCofree (Strong m :: OB (j +-> k)) where
  type Cofree (Strong m) = Star (Tambara m)
  lower' :: forall (a :: j +-> k) (b :: j +-> k).
Cofree (Strong m) a b -> a ~> b
lower' (Star a ~> Tambara m b
n) = (Tambara m b :~> b) -> Prof (Tambara m b) b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof Tambara m b a b -> b a b
Tambara m b :~> b
forall {j} {k} m (p :: j +-> k).
(Profunctor p, MonoidalAction m j, MonoidalAction m k) =>
Tambara m p :~> p
untambara Prof (Tambara m b) b -> Prof a (Tambara m b) -> Prof a b
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Prof b c -> Prof a b -> Prof a c
. a ~> Tambara m b
Prof a (Tambara m b)
n
  section' :: forall (a :: j +-> k) (b :: j +-> k).
Strong m a =>
(a ~> b) -> Cofree (Strong m) a b
section' a ~> b
n = (a ~> Tambara m b) -> Star' ('NT (Tambara m)) a b
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a ~> b) -> Tambara m a ~> Tambara m b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: j +-> k) (b :: j +-> k).
(a ~> b) -> Tambara m a ~> Tambara m b
map a ~> b
n Prof (Tambara m a) (Tambara m b)
-> Prof a (Tambara m a) -> Prof a (Tambara m b)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Prof b c -> Prof a b -> Prof a c
. (a :~> Tambara m a) -> Prof a (Tambara m a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof a a b -> Tambara m a a b
a :~> Tambara m a
forall {j} {k} m (p :: j +-> k).
(Strong m p, MonoidalAction m j, MonoidalAction m k) =>
p :~> Tambara m p
tambara) ((Ob a, Ob b) => Star' ('NT (Tambara m)) a b)
-> Prof a b -> Star' ('NT (Tambara m)) a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j +-> k) (b :: j +-> k) r.
((Ob a, Ob b) => r) -> Prof a b -> r
\\ a ~> b
Prof a b
n

instance (MonoidalAction m j, MonoidalAction m k) => Functor (Tambara m :: (j +-> k) -> (j +-> k)) where
  map :: forall (a :: j +-> k) (b :: j +-> k).
(a ~> b) -> Tambara m a ~> Tambara m b
map (Prof a :~> b
n) = (Tambara m a :~> Tambara m b) -> Prof (Tambara m a) (Tambara m b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Tambara forall (z :: m). Ob z => a (Act z a) (Act z b)
p) -> (forall (z :: m). Ob z => b (Act z a) (Act z b)) -> Tambara m b a b
forall {k} {j} (a :: k) (b :: j) m (p :: j +-> k).
(Ob a, Ob b) =>
(forall (z :: m). Ob z => p (Act z a) (Act z b)) -> Tambara m p a b
Tambara \ @z -> a (Act z a) (Act z b) -> b (Act z a) (Act z b)
a :~> b
n (forall (z :: m). Ob z => a (Act z a) (Act z b)
p @z)
instance (MonoidalAction m j, MonoidalAction m k) => Promonad (Costar (Tambara m) :: (j +-> k) +-> (j +-> k)) where
  id :: forall (a :: j +-> k). Ob a => Costar (Tambara m) a a
id = (Tambara m a ~> a) -> Costar (Tambara m) a a
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar ((Tambara m a :~> a) -> Prof (Tambara m a) a
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof Tambara m a a b -> a a b
Tambara m a :~> a
forall {j} {k} m (p :: j +-> k).
(Profunctor p, MonoidalAction m j, MonoidalAction m k) =>
Tambara m p :~> p
untambara)
  Costar Tambara m b ~> c
n . :: forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Costar (Tambara m) b c
-> Costar (Tambara m) a b -> Costar (Tambara m) a c
. Costar Tambara m a ~> b
m = (Tambara m a ~> c) -> Costar (Tambara m) a c
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar (Tambara m b ~> c
Prof (Tambara m b) c
n Prof (Tambara m b) c
-> Prof (Tambara m a) (Tambara m b) -> Prof (Tambara m 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 (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Prof b c -> Prof a b -> Prof a c
. (Tambara m a ~> b) -> Tambara m (Tambara m a) ~> Tambara m b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: j +-> k) (b :: j +-> k).
(a ~> b) -> Tambara m a ~> Tambara m b
map Tambara m a ~> b
m Prof (Tambara m (Tambara m a)) (Tambara m b)
-> Prof (Tambara m a) (Tambara m (Tambara m a))
-> Prof (Tambara m a) (Tambara m b)
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Prof b c -> Prof a b -> Prof a c
. (Tambara m a :~> Tambara m (Tambara m a))
-> Prof (Tambara m a) (Tambara m (Tambara m a))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof Tambara m a a b -> Tambara m (Tambara m a) a b
Tambara m a :~> Tambara m (Tambara m a)
forall {j} {k} m (p :: j +-> k).
(Strong m p, MonoidalAction m j, MonoidalAction m k) =>
p :~> Tambara m p
tambara)

-- | @Pastro m@ ⊣ @Tambara m@
instance (MonoidalAction m j, MonoidalAction m k) => Corepresentable (Star (Tambara m) :: (j +-> k) +-> (j +-> k)) where
  type Star (Tambara m) %% p = Pastro m p
  coindex :: forall (a :: j +-> k) (b :: j +-> k).
Star (Tambara m) a b -> (Star (Tambara m) %% a) ~> b
coindex (Star (Prof a :~> Tambara m b
n)) = (Pastro m a :~> b) -> Prof (Pastro m a) b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Pastro @z a ~> Act z x
f a x y
p Act z y ~> b
g) -> case a x y -> Tambara m b x y
a :~> Tambara m b
n a x y
p of Tambara forall (z :: m). Ob z => b (Act z x) (Act z y)
q -> (a ~> Act z x) -> (Act z y ~> b) -> b (Act z x) (Act z y) -> b a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> b a b -> b c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> Act z x
f Act z y ~> b
g (forall (z :: m). Ob z => b (Act z x) (Act z y)
q @z)
  cotabulate :: forall (a :: j +-> k) (b :: j +-> k).
Ob a =>
((Star (Tambara m) %% a) ~> b) -> Star (Tambara m) a b
cotabulate (Prof Pastro m a :~> b
n) = (a ~> Tambara m b) -> Star (Tambara m) a b
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a :~> Tambara m b) -> Prof a (Tambara m b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
p -> a a b
p a a b -> ((Ob a, Ob b) => Tambara m b a b) -> Tambara m b a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (z :: m). Ob z => b (Act z a) (Act z b)) -> Tambara m b a b
forall {k} {j} (a :: k) (b :: j) m (p :: j +-> k).
(Ob a, Ob b) =>
(forall (z :: m). Ob z => p (Act z a) (Act z b)) -> Tambara m p a b
Tambara \ @z -> Pastro m a (Act z a) (Act z b) -> b (Act z a) (Act z b)
Pastro m a :~> b
n (forall (z :: m) (x :: k) (y :: j) (p :: j +-> k) (a :: k) (b :: j).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
forall {k} {k} {m} (z :: m) (x :: k) (y :: k) (p :: k +-> k)
       (a :: k) (b :: k).
Ob z =>
(a ~> Act z x) -> p x y -> (Act z y ~> b) -> Pastro m p a b
Pastro @z (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @z Obj z -> (a ~> a) -> Act z a ~> Act z a
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` a a b -> a ~> a
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src a a b
p) a a b
p (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @z Obj z -> (b ~> b) -> Act z b ~> Act z b
forall (a :: m) (b :: m) (x :: j) (y :: j).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` a a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt a a b
p)))
  corepMap :: forall (a :: j +-> k) (b :: j +-> k).
(a ~> b) -> (Star (Tambara m) %% a) ~> (Star (Tambara m) %% b)
corepMap = (a ~> b) -> (Star (Tambara m) %% a) ~> (Star (Tambara m) %% b)
(a ~> b) -> Pastro m a ~> Pastro m b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: j +-> k) (b :: j +-> k).
(a ~> b) -> Pastro m a ~> Pastro m b
map