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

module Proarrow.Profunctor.Instance.PastroTambara where

import Prelude (($))

import Proarrow.Category.Instance.Opposite (OPPOSITE (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (Monoidal (..))
import Proarrow.Category.Monoidal.Action (Act, MonoidalAction (..), actHom, composeActs, decomposeActs)
import Proarrow.Category.Monoidal.Optic (ExOptic (..))
import Proarrow.Category.Monoidal.Strength (Strong (..))
import Proarrow.Core (CategoryOf (..), OB, Profunctor (..), Promonad (..), obj, (//), (:~>), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Profunctor.Cofree (HasCofree (..), cofreeComp)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Free (HasFree (..), freeComp)
import Proarrow.Profunctor.Instance.Costar (Costar, pattern Costar)
import Proarrow.Profunctor.Instance.Star (Star, pattern Star)
import Proarrow.Profunctor.Instance.Yoneda (Yo (..))
import Proarrow.Profunctor.Representable (repObj, withObRep)

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

pastro :: forall {k} t (p :: k +-> k). (Profunctor p, MonoidalAction t) => p :~> Pastro t p
pastro :: forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k).
(Profunctor p, MonoidalAction t) =>
p :~> Pastro t p
pastro p a b
p = forall (z :: m) (x :: k) (y :: k) (p :: k +-> k) (a :: k) (b :: k).
Ob z =>
(a ~> Act t z x) -> p x y -> (Act t z y ~> b) -> Pastro t p a b
forall {m} {k} {t :: (m, k) +-> k} (z :: m) (x :: k) (y :: k)
       (p :: k +-> k) (a :: k) (b :: k).
Ob z =>
(a ~> Act t z x) -> p x y -> (Act t z y ~> b) -> Pastro t p a b
Pastro @Unit (forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
unitorInv @t) p a b
p (forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
unitor @t) ((Ob a, Ob b) => Pastro t p a b) -> p a b -> Pastro t p a b
forall (a :: k) (b :: k) 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 {k} t (p :: k +-> k). (Strong t p, MonoidalAction t) => Pastro t p :~> p
unpastro :: forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k).
(Strong t p, MonoidalAction t) =>
Pastro t p :~> p
unpastro (Pastro @z a ~> Act t z x
f p x y
p Act t z y ~> b
g) = (a ~> Act t z x)
-> (Act t z y ~> b) -> p (Act t z x) (Act t z y) -> p a b
forall (c :: k) (a :: k) (b :: k) (d :: k).
(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 t z x
f Act t z y ~> b
g (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @p @z p x y
p)

instance (CategoryOf k) => Profunctor (Pastro t p :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Pastro t p a b -> Pastro t p c d
dimap c ~> a
l b ~> d
r (Pastro @z a ~> Act t z x
f p x y
p Act t z y ~> b
g) = forall (z :: m) (x :: k) (y :: k) (p :: k +-> k) (a :: k) (b :: k).
Ob z =>
(a ~> Act t z x) -> p x y -> (Act t z y ~> b) -> Pastro t p a b
forall {m} {k} {t :: (m, k) +-> k} (z :: m) (x :: k) (y :: k)
       (p :: k +-> k) (a :: k) (b :: k).
Ob z =>
(a ~> Act t z x) -> p x y -> (Act t z y ~> b) -> Pastro t p a b
Pastro @z (a ~> Act t z x
f (a ~> Act t z x) -> (c ~> a) -> c ~> Act t 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 t z y ~> b) -> Act t z y ~> d
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
. Act t z y ~> b
g)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> Pastro t p a b -> r
\\ Pastro a ~> Act t z x
f p x y
_ Act t z y ~> b
g = r
(Ob a, Ob b) => r
(Ob a, Ob (Act t z x)) => r
r ((Ob a, Ob (Act t z x)) => r) -> (a ~> Act t 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 t z x
f ((Ob (Act t z y), Ob b) => r) -> (Act t z y ~> b) -> 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
\\ Act t z y ~> b
g
instance (MonoidalAction t, Profunctor p) => Strong t (Pastro t p :: k +-> k) where
  act :: forall (a :: m) (x :: k) (y :: k).
Ob a =>
Pastro t p x y -> Pastro t p (Act t a x) (Act t a y)
act @a @x @y (Pastro @z @x1 @y1 x ~> Act t z x
f p x y
p Act t z y ~> y
g) =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @z
      (forall (z :: m) (x :: k) (y :: k) (p :: k +-> k) (a :: k) (b :: k).
Ob z =>
(a ~> Act t z x) -> p x y -> (Act t z y ~> b) -> Pastro t p a b
forall {m} {k} {t :: (m, k) +-> k} (z :: m) (x :: k) (y :: k)
       (p :: k +-> k) (a :: k) (b :: k).
Ob z =>
(a ~> Act t z x) -> p x y -> (Act t z y ~> b) -> Pastro t p a b
Pastro @(a ** z) (forall {m} {k} (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k)
       (a :: k) (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(a ~> Act t x b) -> (b ~> Act t y c) -> a ~> Act t (x ** y) c
forall (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k) (a :: k)
       (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(a ~> Act t x b) -> (b ~> Act t y c) -> a ~> Act t (x ** y) c
composeActs @t @a @z @x1 (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: (m, k) +-> k) (a :: (m, k)).
(Representable p, Ob a) =>
Obj (p % a)
repObj @t @'(a, x)) x ~> Act t z x
f) p x y
p (forall {m} {k} (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k)
       (a :: k) (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(Act t y c ~> b) -> (Act t x b ~> a) -> Act t (x ** y) c ~> a
forall (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k) (a :: k)
       (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(Act t y c ~> b) -> (Act t x b ~> a) -> Act t (x ** y) c ~> a
decomposeActs @t @a @z @y1 Act t z y ~> y
g (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: (m, k) +-> k) (a :: (m, k)).
(Representable p, Ob a) =>
Obj (p % a)
repObj @t @'(a, y))))
      ((Ob x, Ob (Act t z x)) => Pastro t p (t % '(a, x)) (t % '(a, y)))
-> (x ~> Act t z x) -> Pastro t p (t % '(a, x)) (t % '(a, 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 t z x
f
      ((Ob (Act t z y), Ob y) => Pastro t p (t % '(a, x)) (t % '(a, y)))
-> (Act t z y ~> y) -> Pastro t p (t % '(a, x)) (t % '(a, 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
\\ Act t z y ~> y
g
      ((Ob x, Ob y) => Pastro t p (t % '(a, x)) (t % '(a, y)))
-> p x y -> Pastro t p (t % '(a, x)) (t % '(a, y))
forall (a :: k) (b :: k) 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 t) => HasFree (Strong t :: OB (k +-> k)) where
  type Free (Strong t) p = Pastro t p
  lift :: forall (a :: k +-> k). Ob a => a ~> Free (Strong t) a
lift = (a :~> Pastro t a) -> Prof a (Pastro t a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof a a b -> Pastro t a a b
a :~> Pastro t a
forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k).
(Profunctor p, MonoidalAction t) =>
p :~> Pastro t p
pastro
  foldMap :: forall (b :: k +-> k) (a :: k +-> k).
Strong t b =>
(a ~> b) -> Free (Strong t) a ~> b
foldMap a ~> b
n = (Pastro t b :~> b) -> Prof (Pastro t b) b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof Pastro t b a b -> b a b
Pastro t b :~> b
forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k).
(Strong t p, MonoidalAction t) =>
Pastro t p :~> p
unpastro Prof (Pastro t b) b
-> Prof (Pastro t a) (Pastro t b) -> Prof (Pastro t 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 :: k +-> k) (c :: k +-> k) (a :: k +-> k).
Prof b c -> Prof a b -> Prof a c
. (a ~> b) -> Pastro t a ~> Pastro t b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k +-> k) (b :: k +-> k).
(a ~> b) -> Pastro t a ~> Pastro t b
map a ~> b
n

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

fromWeightedOptic
  :: forall {k} t (a :: k) (b :: k)
   . (MonoidalAction t) => ExOptic t a b :~> (Pastro t (Yo a (OP b)) :: k +-> k)
fromWeightedOptic :: forall {m} {k} (t :: (m, k) +-> k) (a :: k) (b :: k).
MonoidalAction t =>
ExOptic t a b :~> Pastro t (Yo a ('OP b))
fromWeightedOptic (ExOptic @x a ~> Act t x a
f Act t x b ~> b
g) = forall (z :: m) (x :: k) (y :: k) (p :: k +-> k) (a :: k) (b :: k).
Ob z =>
(a ~> Act t z x) -> p x y -> (Act t z y ~> b) -> Pastro t p a b
forall {m} {k} {t :: (m, k) +-> k} (z :: m) (x :: k) (y :: k)
       (p :: k +-> k) (a :: k) (b :: k).
Ob z =>
(a ~> Act t z x) -> p x y -> (Act t z y ~> b) -> Pastro t p a b
Pastro @x a ~> Act t 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 :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id) Act t x b ~> b
g

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

tambara :: forall {k} t (p :: k +-> k). (Strong t p, MonoidalAction t) => p :~> Tambara t p
tambara :: forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k).
(Strong t p, MonoidalAction t) =>
p :~> Tambara t p
tambara p a b
p = (forall (z :: m). Ob z => p (Act t z a) (Act t z b))
-> Tambara t p a b
forall {k} (a :: k) (b :: k) m (p :: k +-> k) (t :: (m, k) +-> k).
(Ob a, Ob b) =>
(forall (z :: m). Ob z => p (Act t z a) (Act t z b))
-> Tambara t p a b
Tambara (\ @z -> forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @p @z p a b
p) ((Ob a, Ob b) => Tambara t p a b) -> p a b -> Tambara t p a b
forall (a :: k) (b :: k) 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 {k} t (p :: k +-> k). (Profunctor p, MonoidalAction t) => Tambara t p :~> p
untambara :: forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k).
(Profunctor p, MonoidalAction t) =>
Tambara t p :~> p
untambara (Tambara forall (z :: m). Ob z => p (Act t z a) (Act t z b)
p) = (a ~> (t % '(Unit, a)))
-> ((t % '(Unit, b)) ~> b)
-> p (t % '(Unit, a)) (t % '(Unit, b))
-> p a b
forall (c :: k) (a :: k) (b :: k) (d :: k).
(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} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
unitorInv @t) (forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
unitor @t) (forall (z :: m). Ob z => p (Act t z a) (Act t z b)
p @Unit)

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

instance (MonoidalAction t) => HasCofree (Strong t :: OB (k +-> k)) where
  type Cofree (Strong t) p = Tambara t p
  lower :: forall (a :: k +-> k). Ob a => Cofree (Strong t) a ~> a
lower = (Tambara t a :~> a) -> Prof (Tambara t a) a
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof Tambara t a a b -> a a b
Tambara t a :~> a
forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k).
(Profunctor p, MonoidalAction t) =>
Tambara t p :~> p
untambara
  unfoldMap :: forall (a :: k +-> k) (b :: k +-> k).
Strong t a =>
(a ~> b) -> a ~> Cofree (Strong t) b
unfoldMap a ~> b
n = (a ~> b) -> Tambara t a ~> Tambara t b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k +-> k) (b :: k +-> k).
(a ~> b) -> Tambara t a ~> Tambara t b
map a ~> b
n Prof (Tambara t a) (Tambara t b)
-> Prof a (Tambara t a) -> Prof a (Tambara t 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 :: k +-> k) (c :: k +-> k) (a :: k +-> k).
Prof b c -> Prof a b -> Prof a c
. (a :~> Tambara t a) -> Prof a (Tambara t a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof a a b -> Tambara t a a b
a :~> Tambara t a
forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k).
(Strong t p, MonoidalAction t) =>
p :~> Tambara t p
tambara

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

-- | @Pastro t@ ⊣ @Tambara t@
instance (MonoidalAction t) => Corepresentable (Star (Tambara t) :: (k +-> k) +-> (k +-> k)) where
  type Star (Tambara t) %% p = Pastro t p
  coindex :: forall (a :: k +-> k) (b :: k +-> k).
Star (Tambara t) a b -> (Star (Tambara t) %% a) ~> b
coindex (Star (Prof a :~> Tambara t b
n)) = (Pastro t a :~> b) -> Prof (Pastro t 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 t z x
f a x y
p Act t z y ~> b
g) -> case a x y -> Tambara t b x y
a :~> Tambara t b
n a x y
p of Tambara forall (z :: m). Ob z => b (Act t z x) (Act t z y)
q -> (a ~> Act t z x)
-> (Act t z y ~> b) -> b (Act t z x) (Act t z y) -> b a b
forall (c :: k) (a :: k) (b :: k) (d :: k).
(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 t z x
f Act t z y ~> b
g (forall (z :: m). Ob z => b (Act t z x) (Act t z y)
q @z)
  cotabulate :: forall (a :: k +-> k) (b :: k +-> k).
Ob a =>
((Star (Tambara t) %% a) ~> b) -> Star (Tambara t) a b
cotabulate (Prof Pastro t a :~> b
n) = (a ~> Tambara t b) -> Star (Tambara t) a b
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a :~> Tambara t b) -> Prof a (Tambara t b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \ @a @b a a b
p -> a a b
p a a b -> ((Ob a, Ob b) => Tambara t b a b) -> Tambara t 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 t z a) (Act t z b))
-> Tambara t b a b
forall {k} (a :: k) (b :: k) m (p :: k +-> k) (t :: (m, k) +-> k).
(Ob a, Ob b) =>
(forall (z :: m). Ob z => p (Act t z a) (Act t z b))
-> Tambara t p a b
Tambara \ @z -> Pastro t a (Act t z a) (Act t z b) -> b (Act t z a) (Act t z b)
Pastro t a :~> b
n (forall (z :: m) (x :: k) (y :: k) (p :: k +-> k) (a :: k) (b :: k).
Ob z =>
(a ~> Act t z x) -> p x y -> (Act t z y ~> b) -> Pastro t p a b
forall {m} {k} {t :: (m, k) +-> k} (z :: m) (x :: k) (y :: k)
       (p :: k +-> k) (a :: k) (b :: k).
Ob z =>
(a ~> Act t z x) -> p x y -> (Act t z y ~> b) -> Pastro t p a b
Pastro @z (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: (m, k) +-> k) (a :: (m, k)).
(Representable p, Ob a) =>
Obj (p % a)
repObj @t @'(z, a)) a a b
p (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: (m, k) +-> k) (a :: (m, k)).
(Representable p, Ob a) =>
Obj (p % a)
repObj @t @'(z, b))))
  corepMap :: forall (a :: k +-> k) (b :: k +-> k).
(a ~> b) -> (Star (Tambara t) %% a) ~> (Star (Tambara t) %% b)
corepMap = (a ~> b) -> (Star (Tambara t) %% a) ~> (Star (Tambara t) %% b)
(a ~> b) -> Pastro t a ~> Pastro t b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: k +-> k) (b :: k +-> k).
(a ~> b) -> Pastro t a ~> Pastro t b
map