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

-- | 'Pastro' and 'Tambara' are the free and cofree 'Prostrong' profunctors for an optic flavor @w@ (the
-- 'HasFree' and 'HasCofree' instances for @'Prostrong' w@): @Pastro w r@ sandwiches @r@ between an
-- existential witness pair, while @Tambara w r@ provides strength against every witness pair at once.
module Proarrow.Profunctor.Instance.PastroTambara where

import Prelude (($))

import Proarrow.Category.Instance.Opposite (OPPOSITE (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Core (CategoryOf (..), OB, Profunctor (..), Promonad (..), src, tgt, (//), (:~>), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Optic (ExOptic (..), FLAVOR, Flavor, Prostrong (..))
import Proarrow.Profunctor.Cofree (HasCofree (..), cofreeComp)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Free (HasFree (..), freeComp)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Costar (Costar, pattern Costar)
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Ran (Ran (..), runRan, type (|>))
import Proarrow.Profunctor.Instance.Rift (Rift (..), runRift, type (<|))
import Proarrow.Profunctor.Instance.Star (Star, pattern Star)
import Proarrow.Profunctor.Instance.Yoneda (Yo (..))

-- | The free 'Prostrong' profunctor for the flavor @w@: the profunctor @r@ sandwiched between an
-- existential @w@-witness pair.
type Pastro :: FLAVOR j k -> j +-> k -> j +-> k
data Pastro w r a b where
  Pastro
    :: forall {k} {j} (p :: k +-> k) (q :: j +-> j) w r a b
     . (w p q, Profunctor p, Profunctor q) => (p :.: r :.: q) a b -> Pastro w r a b

pastro :: forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k). (Profunctor p, Flavor w) => p :~> Pastro w p
pastro :: forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k).
(Profunctor p, Flavor w) =>
p :~> Pastro w p
pastro p a b
p = (:.:) (Id :.: p) Id a b -> Pastro w p a b
forall {k} {j} (p :: k +-> k) (q :: j +-> j)
       (w :: (k +-> k) -> (j +-> j) -> Constraint) (r :: j +-> k) (a :: k)
       (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: r) q a b -> Pastro w r a b
Pastro ((a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id Id a a -> p a b -> (:.:) Id p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p a b
p (:.:) Id p a b -> Id b b -> (:.:) (Id :.: p) Id a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id) ((Ob a, Ob b) => Pastro w p a b) -> p a b -> Pastro w 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} (w :: FLAVOR j k) (p :: j +-> k). (Prostrong w p) => Pastro w p :~> p
unpastro :: forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k).
Prostrong w p =>
Pastro w p :~> p
unpastro (Pastro (:.:) (p :.: p) q a b
fpg) = forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k) (f :: k +-> k)
       (g :: j +-> j).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
forall (w :: FLAVOR j k) (p :: j +-> k) (f :: k +-> k)
       (g :: j +-> j).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
proact @w (:.:) (p :.: p) q a b
fpg

instance (CategoryOf j, CategoryOf k, Profunctor p) => Profunctor (Pastro t p :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Pastro t p a b -> Pastro t p c d
dimap c ~> a
l b ~> d
r (Pastro (:.:) (p :.: p) q a b
fpg) = (:.:) (p :.: p) q c d -> Pastro t p c d
forall {k} {j} (p :: k +-> k) (q :: j +-> j)
       (w :: (k +-> k) -> (j +-> j) -> Constraint) (r :: j +-> k) (a :: k)
       (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: r) q a b -> Pastro w r a b
Pastro ((c ~> a)
-> (b ~> d) -> (:.:) (p :.: p) q a b -> (:.:) (p :.: p) q c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> (:.:) (p :.: p) q a b -> (:.:) (p :.: p) q 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 c ~> a
l b ~> d
r (:.:) (p :.: p) q a b
fpg)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Pastro t p a b -> r
\\ Pastro (:.:) (p :.: p) q a b
fpg = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (:.:) (p :.: p) q a b -> r
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> (:.:) (p :.: p) q 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 :.: p) q a b
fpg
instance (Flavor w, Profunctor p) => Prostrong w (Pastro w p :: j +-> k) where
  proact :: forall (f :: k +-> k) (g :: j +-> j).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Pastro w p) :.: g) :~> Pastro w p
proact (f a b
p :.: Pastro (p b b
p' :.: p b b
r :.: q b b
q') :.: g b b
q) = (:.:) ((f :.: p) :.: p) (q :.: g) a b -> Pastro w p a b
forall {k} {j} (p :: k +-> k) (q :: j +-> j)
       (w :: (k +-> k) -> (j +-> j) -> Constraint) (r :: j +-> k) (a :: k)
       (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: r) q a b -> Pastro w r a b
Pastro ((f a b
p f a b -> p b b -> (:.:) f p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
p') (:.:) f p a b -> p b b -> (:.:) (f :.: p) p a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r (:.:) (f :.: p) p a b
-> (:.:) q g b b -> (:.:) ((f :.: p) :.: p) (q :.: g) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (q b b
q' q b b -> g b b -> (:.:) q g b b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: g b b
q))

instance (Flavor w) => HasFree (Prostrong w :: OB (j +-> k)) where
  type Free (Prostrong w) p = Pastro w p
  lift :: forall (a :: j +-> k). Ob a => a ~> Free (Prostrong w) a
lift = (a :~> Pastro w a) -> Prof a (Pastro w a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof a a b -> Pastro w a a b
a :~> Pastro w a
forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k).
(Profunctor p, Flavor w) =>
p :~> Pastro w p
pastro
  foldMap :: forall (b :: j +-> k) (a :: j +-> k).
Prostrong w b =>
(a ~> b) -> Free (Prostrong w) a ~> b
foldMap a ~> b
n = (Pastro w b :~> b) -> Prof (Pastro w b) b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof Pastro w b a b -> b a b
Pastro w b :~> b
forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k).
Prostrong w p =>
Pastro w p :~> p
unpastro Prof (Pastro w b) b
-> Prof (Pastro w a) (Pastro w b) -> Prof (Pastro w a) b
forall {k} (p :: CAT 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) -> Pastro w a ~> Pastro w 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 w a ~> Pastro w b
map a ~> b
n

instance Functor (Pastro t) where
  map :: forall (a :: k -> j -> Type) (b :: k -> j -> 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 (p a b
f :.: a b b
p :.: q b b
g)) -> (:.:) (p :.: b) q a b -> Pastro t b a b
forall {k} {j} (p :: k +-> k) (q :: j +-> j)
       (w :: (k +-> k) -> (j +-> j) -> Constraint) (r :: j +-> k) (a :: k)
       (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: r) q a b -> Pastro w r a b
Pastro (p a b
f p a b -> b b b -> (:.:) p b a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: a b b -> b b b
a :~> b
n a b b
p (:.:) p b a b -> q b b -> (:.:) (p :.: b) q a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b b
g)
instance (Flavor w) => Promonad (Star (Pastro w) :: (j +-> k) +-> (j +-> k)) where
  id :: forall (a :: j +-> k). Ob a => Star (Pastro w) a a
id = (a ~> Pastro w a) -> Star (Pastro w) a a
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a :~> Pastro w a) -> Prof a (Pastro w a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof a a b -> Pastro w a a b
a :~> Pastro w a
forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k).
(Profunctor p, Flavor w) =>
p :~> Pastro w p
pastro)
  Star b ~> Pastro w c
n . :: forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Star (Pastro w) b c -> Star (Pastro w) a b -> Star (Pastro w) a c
. Star a ~> Pastro w b
m = (a ~> Pastro w c) -> Star (Pastro w) 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 (j +-> k)) (c :: j +-> k) (b :: j +-> k)
       (a :: j +-> k).
(HasFree ob, Ob c) =>
(b ~> Free ob c) -> (a ~> Free ob b) -> a ~> Free ob c
freeComp @(Prostrong w) b ~> Free (Prostrong w) c
b ~> Pastro w c
n a ~> Free (Prostrong w) b
a ~> Pastro w b
m)

fromExOptic
  :: forall {j} {k} w (a :: k) (b :: j)
   . (CategoryOf j, CategoryOf k) => ExOptic w a b :~> (Pastro w (Yo a (OP b)) :: j +-> k)
fromExOptic :: forall {j} {k} (w :: FLAVOR j k) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b :~> Pastro w (Yo a (OP b))
fromExOptic (ExOptic p a a
f q b b
g) = (:.:) (p :.: Yo a (OP b)) q a b -> Pastro w (Yo a (OP b)) a b
forall {k} {j} (p :: k +-> k) (q :: j +-> j)
       (w :: (k +-> k) -> (j +-> j) -> Constraint) (r :: j +-> k) (a :: k)
       (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: r) q a b -> Pastro w r a b
Pastro (p a a
f p a a -> Yo a (OP b) a b -> (:.:) p (Yo a (OP b)) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (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 (p a a -> a ~> a
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt p a a
f) (q b b -> b ~> b
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src q b b
g) (:.:) p (Yo a (OP b)) a b
-> q b b -> (:.:) (p :.: Yo a (OP b)) q a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b b
g)

-- | The cofree 'Prostrong' profunctor for the flavor @w@: strength against every @w@-witness pair
-- at once.
type Tambara :: FLAVOR j k -> j +-> k -> j +-> k
data Tambara w r a b where
  Tambara
    :: forall {j} {k} (w :: FLAVOR j k) (r :: j +-> k) a b
     . (Ob a, Ob b)
    => (forall (p :: k +-> k) (q :: j +-> j). (w p q, Profunctor p, Profunctor q) => (q |> r <| p) a b)
    -> Tambara w r a b

mkTambara
  :: (Ob a, Ob b)
  => (forall (p :: k +-> k) (q :: j +-> j) x y. (w p q, Profunctor p, Profunctor q) => p x a -> q b y -> r x y)
  -> Tambara w r a b
mkTambara :: forall k (a :: k) j (b :: j) (w :: FLAVOR j k) (r :: j +-> k).
(Ob a, Ob b) =>
(forall (p :: k +-> k) (q :: j +-> j) (x :: k) (y :: j).
 (w p q, Profunctor p, Profunctor q) =>
 p x a -> q b y -> r x y)
-> Tambara w r a b
mkTambara forall (p :: k +-> k) (q :: j +-> j) (x :: k) (y :: j).
(w p q, Profunctor p, Profunctor q) =>
p x a -> q b y -> r x y
f = (forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 (<|) (q |> r) p a b)
-> Tambara w r a b
forall {j} {k} (w :: FLAVOR j k) (r :: j +-> k) (a :: k) (b :: j).
(Ob a, Ob b) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 (<|) (q |> r) p a b)
-> Tambara w r a b
Tambara ((forall (x :: k). p x a -> (|>) q r x b)
-> Rift (OP p) (q |> r) a b
forall {k} {j} {i} (a :: k) (b :: j) (j2 :: k +-> i)
       (p :: j +-> i).
(Ob a, Ob b) =>
(forall (x :: i). j2 x a -> p x b) -> Rift (OP j2) p a b
Rift \p x a
p -> p x a
p p x a -> ((Ob x, Ob a) => (|>) q r x b) -> (|>) q r x b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (x :: j). q b x -> r x x) -> (|>) q r x b
forall {k} {j} {i} (a :: k) (b :: j) (j2 :: i +-> j)
       (p :: i +-> k).
(Ob a, Ob b) =>
(forall (x :: i). j2 b x -> p a x) -> Ran (OP j2) p a b
Ran \q b x
q -> p x a -> q b x -> r x x
forall (p :: k +-> k) (q :: j +-> j) (x :: k) (y :: j).
(w p q, Profunctor p, Profunctor q) =>
p x a -> q b y -> r x y
f p x a
p q b x
q)

runTambara :: (w p q, Profunctor p, Profunctor q) => ((Ob a) => p x a) -> ((Ob b) => q b y) -> Tambara w r a b -> r x y
runTambara :: forall {k} {j} (w :: (k +-> k) -> (j +-> j) -> Constraint)
       (p :: k +-> k) (q :: j +-> j) (a :: k) (x :: k) (b :: j) (y :: j)
       (r :: j +-> k).
(w p q, Profunctor p, Profunctor q) =>
(Ob a => p x a) -> (Ob b => q b y) -> Tambara w r a b -> r x y
runTambara Ob a => p x a
p Ob b => q b y
q (Tambara forall (p :: k +-> k) (q :: j +-> j).
(w p q, Profunctor p, Profunctor q) =>
(<|) (q |> r) p a b
qrp) = q b y -> Ran (OP q) r x b -> r x y
forall {i} {j1} {k} (j2 :: i +-> j1) (b :: j1) (x :: i)
       (p :: i +-> k) (a :: k).
Profunctor j2 =>
j2 b x -> Ran (OP j2) p a b -> p a x
runRan q b y
Ob b => q b y
q (Ran (OP q) r x b -> r x y) -> Ran (OP q) r x b -> r x y
forall a b. (a -> b) -> a -> b
$ p x a -> Rift (OP p) (Ran (OP q) r) a b -> Ran (OP q) r x b
forall {k} {i} {j1} (j2 :: k +-> i) (x :: i) (a :: k)
       (p :: j1 +-> i) (b :: j1).
Profunctor j2 =>
j2 x a -> Rift (OP j2) p a b -> p x b
runRift p x a
Ob a => p x a
p Rift (OP p) (Ran (OP q) r) a b
forall (p :: k +-> k) (q :: j +-> j).
(w p q, Profunctor p, Profunctor q) =>
(<|) (q |> r) p a b
qrp

tambara :: forall {j} {k} w (p :: j +-> k). (Prostrong w p) => p :~> Tambara w p
tambara :: forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k).
Prostrong w p =>
p :~> Tambara w p
tambara p a b
r = (forall (p :: k +-> k) (q :: j +-> j) (x :: k) (y :: j).
 (w p q, Profunctor p, Profunctor q) =>
 p x a -> q b y -> p x y)
-> Tambara w p a b
forall k (a :: k) j (b :: j) (w :: FLAVOR j k) (r :: j +-> k).
(Ob a, Ob b) =>
(forall (p :: k +-> k) (q :: j +-> j) (x :: k) (y :: j).
 (w p q, Profunctor p, Profunctor q) =>
 p x a -> q b y -> r x y)
-> Tambara w r a b
mkTambara (\p x a
p q b y
q -> forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k) (f :: k +-> k)
       (g :: j +-> j).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
forall (w :: FLAVOR j k) (p :: j +-> k) (f :: k +-> k)
       (g :: j +-> j).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
proact @w (p x a
p p x a -> p a b -> (:.:) p p x b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p a b
r (:.:) p p x b -> q b y -> (:.:) (p :.: p) q x y
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b y
q)) ((Ob a, Ob b) => Tambara w p a b) -> p a b -> Tambara w 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
r

untambara
  :: forall {j} {k} w (p :: j +-> k). (Profunctor p, Flavor w) => Tambara w p :~> p
untambara :: forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k).
(Profunctor p, Flavor w) =>
Tambara w p :~> p
untambara = forall {k} {j} (w :: (k +-> k) -> (j +-> j) -> Constraint)
       (p :: k +-> k) (q :: j +-> j) (a :: k) (x :: k) (b :: j) (y :: j)
       (r :: j +-> k).
(w p q, Profunctor p, Profunctor q) =>
(Ob a => p x a) -> (Ob b => q b y) -> Tambara w r a b -> r x y
forall (w :: (k +-> k) -> (j +-> j) -> Constraint) (p :: k +-> k)
       (q :: j +-> j) (a :: k) (x :: k) (b :: j) (y :: j) (r :: j +-> k).
(w p q, Profunctor p, Profunctor q) =>
(Ob a => p x a) -> (Ob b => q b y) -> Tambara w r a b -> r x y
runTambara @w @Id @Id ((a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id) ((b ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)

instance (Profunctor p) => Profunctor (Tambara w p :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Tambara w p a b -> Tambara w p c d
dimap c ~> a
l b ~> d
r (Tambara forall (p :: k +-> k) (q :: j +-> j).
(w p q, Profunctor p, Profunctor q) =>
(<|) (q |> p) p a b
n) = (forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 (<|) (q |> p) p c d)
-> Tambara w p c d
forall {j} {k} (w :: FLAVOR j k) (r :: j +-> k) (a :: k) (b :: j).
(Ob a, Ob b) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 (<|) (q |> r) p a b)
-> Tambara w r a b
Tambara ((c ~> a)
-> (b ~> d) -> Rift (OP p) (q |> p) a b -> Rift (OP p) (q |> p) c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> Rift (OP p) (q |> p) a b -> Rift (OP p) (q |> 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 c ~> a
l b ~> d
r Rift (OP p) (q |> p) a b
forall (p :: k +-> k) (q :: j +-> j).
(w p q, Profunctor p, Profunctor q) =>
(<|) (q |> p) p a b
n) ((Ob c, Ob a) => Tambara w p c d) -> (c ~> a) -> Tambara w 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 w p c d) -> (b ~> d) -> Tambara w 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 w p a b -> r
\\ Tambara{} = r
(Ob a, Ob b) => r
r

instance (Flavor w, Profunctor p) => Prostrong w (Tambara w p :: j +-> k) where
  proact :: forall (f :: k +-> k) (g :: j +-> j).
(w f g, Profunctor f, Profunctor g) =>
((f :.: Tambara w p) :.: g) :~> Tambara w p
proact (f a b
p :.: Tambara w p b b
n :.: g b b
q) = (forall (p :: k +-> k) (q :: j +-> j) (x :: k) (y :: j).
 (w p q, Profunctor p, Profunctor q) =>
 p x a -> q b y -> p x y)
-> Tambara w p a b
forall k (a :: k) j (b :: j) (w :: FLAVOR j k) (r :: j +-> k).
(Ob a, Ob b) =>
(forall (p :: k +-> k) (q :: j +-> j) (x :: k) (y :: j).
 (w p q, Profunctor p, Profunctor q) =>
 p x a -> q b y -> r x y)
-> Tambara w r a b
mkTambara (\p x a
p' q b y
q' -> (Ob b => (:.:) p f x b)
-> (Ob b => (:.:) g q b y) -> Tambara w p b b -> p x y
forall {k} {j} (w :: (k +-> k) -> (j +-> j) -> Constraint)
       (p :: k +-> k) (q :: j +-> j) (a :: k) (x :: k) (b :: j) (y :: j)
       (r :: j +-> k).
(w p q, Profunctor p, Profunctor q) =>
(Ob a => p x a) -> (Ob b => q b y) -> Tambara w r a b -> r x y
runTambara (p x a
p' p x a -> f a b -> (:.:) p f x b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: f a b
p) (g b b
q g b b -> q b y -> (:.:) g q b y
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b y
q') Tambara w p b b
n) ((Ob a, Ob b) => Tambara w p a b) -> f a b -> Tambara w p a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> f 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
\\ f a b
p ((Ob b, Ob b) => Tambara w p a b) -> g b b -> Tambara w p a b
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> g 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
\\ g b b
q

instance (Flavor w) => HasCofree (Prostrong w :: OB (j +-> k)) where
  type Cofree (Prostrong w) p = Tambara w p
  lower :: forall (a :: j +-> k). Ob a => Cofree (Prostrong w) a ~> a
lower = (Tambara w a :~> a) -> Prof (Tambara w a) a
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof Tambara w a a b -> a a b
Tambara w a :~> a
forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k).
(Profunctor p, Flavor w) =>
Tambara w p :~> p
untambara
  unfoldMap :: forall (a :: j +-> k) (b :: j +-> k).
Prostrong w a =>
(a ~> b) -> a ~> Cofree (Prostrong w) b
unfoldMap a ~> b
n = (a ~> b) -> Tambara w a ~> Tambara w 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 w a ~> Tambara w b
map a ~> b
n Prof (Tambara w a) (Tambara w b)
-> Prof a (Tambara w a) -> Prof a (Tambara w b)
forall {k} (p :: CAT 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 w a) -> Prof a (Tambara w a)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof a a b -> Tambara w a a b
a :~> Tambara w a
forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k).
Prostrong w p =>
p :~> Tambara w p
tambara

instance Functor (Tambara w :: (j +-> k) -> (j +-> k)) where
  map :: forall (a :: j +-> k) (b :: j +-> k).
(a ~> b) -> Tambara w a ~> Tambara w b
map (Prof a :~> b
n) = (Tambara w a :~> Tambara w b) -> Prof (Tambara w a) (Tambara w b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \Tambara w a a b
t -> Tambara w a a b
t Tambara w a a b
-> ((Ob a, Ob b) => Tambara w b a b) -> Tambara w 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 (p :: k +-> k) (q :: j +-> j) (x :: k) (y :: j).
 (w p q, Profunctor p, Profunctor q) =>
 p x a -> q b y -> b x y)
-> Tambara w b a b
forall k (a :: k) j (b :: j) (w :: FLAVOR j k) (r :: j +-> k).
(Ob a, Ob b) =>
(forall (p :: k +-> k) (q :: j +-> j) (x :: k) (y :: j).
 (w p q, Profunctor p, Profunctor q) =>
 p x a -> q b y -> r x y)
-> Tambara w r a b
mkTambara \p x a
p q b y
q -> a x y -> b x y
a :~> b
n ((Ob a => p x a) -> (Ob b => q b y) -> Tambara w a a b -> a x y
forall {k} {j} (w :: (k +-> k) -> (j +-> j) -> Constraint)
       (p :: k +-> k) (q :: j +-> j) (a :: k) (x :: k) (b :: j) (y :: j)
       (r :: j +-> k).
(w p q, Profunctor p, Profunctor q) =>
(Ob a => p x a) -> (Ob b => q b y) -> Tambara w r a b -> r x y
runTambara p x a
Ob a => p x a
p q b y
Ob b => q b y
q Tambara w a a b
t)
instance (Flavor w) => Promonad (Costar (Tambara w) :: (j +-> k) +-> (j +-> k)) where
  id :: forall (a :: j +-> k). Ob a => Costar (Tambara w) a a
id = (Tambara w a ~> a) -> Costar (Tambara w) a a
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar ((Tambara w a :~> a) -> Prof (Tambara w a) a
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof Tambara w a a b -> a a b
Tambara w a :~> a
forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k).
(Profunctor p, Flavor w) =>
Tambara w p :~> p
untambara)
  Costar Tambara w b ~> c
n . :: forall (b :: j +-> k) (c :: j +-> k) (a :: j +-> k).
Costar (Tambara w) b c
-> Costar (Tambara w) a b -> Costar (Tambara w) a c
. Costar Tambara w a ~> b
m = (Tambara w a ~> c) -> Costar (Tambara w) 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 (j +-> k)) (a :: j +-> k) (b :: j +-> k)
       (c :: j +-> k).
(HasCofree ob, Ob a) =>
(Cofree ob b ~> c) -> (Cofree ob a ~> b) -> Cofree ob a ~> c
cofreeComp @(Prostrong w) Cofree (Prostrong w) b ~> c
Tambara w b ~> c
n Cofree (Prostrong w) a ~> b
Tambara w a ~> b
m)

-- | @Pastro t@ ⊣ @Tambara t@
instance Corepresentable (Star (Tambara w) :: (j +-> k) +-> (j +-> k)) where
  type Star (Tambara w) %% p = Pastro w p
  coindex :: forall (a :: j +-> k) (b :: j +-> k).
Star (Tambara w) a b -> (Star (Tambara w) %% a) ~> b
coindex (Star (Prof a :~> Tambara w b
n)) = (Pastro w a :~> b) -> Prof (Pastro w a) b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Pastro @p @q (p a b
p :.: a b b
r :.: q b b
q)) -> case a b b -> Tambara w b b b
a :~> Tambara w b
n a b b
r of Tambara w b b b
m -> forall {k} {j} (w :: (k +-> k) -> (j +-> j) -> Constraint)
       (p :: k +-> k) (q :: j +-> j) (a :: k) (x :: k) (b :: j) (y :: j)
       (r :: j +-> k).
(w p q, Profunctor p, Profunctor q) =>
(Ob a => p x a) -> (Ob b => q b y) -> Tambara w r a b -> r x y
forall (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j) (a :: k)
       (x :: k) (b :: j) (y :: j) (r :: j +-> k).
(w p q, Profunctor p, Profunctor q) =>
(Ob a => p x a) -> (Ob b => q b y) -> Tambara w r a b -> r x y
runTambara @w @p @q p a b
Ob b => p a b
p q b b
Ob b => q b b
q Tambara w b b b
m
  corepUniv :: forall (a :: j +-> k).
Ob a =>
Star (Tambara w) a (Star (Tambara w) %% a)
corepUniv = (a ~> Tambara w (Pastro w a)) -> Star (Tambara w) a (Pastro w a)
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star ((a :~> Tambara w (Pastro w a)) -> Prof a (Tambara w (Pastro w a))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
r -> a a b
r a a b
-> ((Ob a, Ob b) => Tambara w (Pastro w a) a b)
-> Tambara w (Pastro w a) 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 (p :: k +-> k) (q :: j +-> j) (x :: k) (y :: j).
 (w p q, Profunctor p, Profunctor q) =>
 p x a -> q b y -> Pastro w a x y)
-> Tambara w (Pastro w a) a b
forall k (a :: k) j (b :: j) (w :: FLAVOR j k) (r :: j +-> k).
(Ob a, Ob b) =>
(forall (p :: k +-> k) (q :: j +-> j) (x :: k) (y :: j).
 (w p q, Profunctor p, Profunctor q) =>
 p x a -> q b y -> r x y)
-> Tambara w r a b
mkTambara \p x a
p q b y
q -> (:.:) (p :.: a) q x y -> Pastro w a x y
forall {k} {j} (p :: k +-> k) (q :: j +-> j)
       (w :: (k +-> k) -> (j +-> j) -> Constraint) (r :: j +-> k) (a :: k)
       (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: r) q a b -> Pastro w r a b
Pastro (p x a
p p x a -> a a b -> (:.:) p a x b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: a a b
r (:.:) p a x b -> q b y -> (:.:) (p :.: a) q x y
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q b y
q))