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

-- | The __traversal__: the many-focus optic, distributing any
-- 'Proarrow.Category.Monoidal.Distributive.StrongDistributiveProfunctor' with product strength
-- through the foci. This module keeps the mutually-recursive 'TravRes'\/'MonTravRes' flavor
-- classes and their leaf witnesses ('Traversable' and 'Cotraversable' functors, the product lens,
-- the coproduct prism, 'Beside'\/'BesideSum' juxtaposition and the unit\/zero witnesses); the
-- free-profunctor apparatus lives in "Proarrow.Optic.MonoidalTraversal". A traversal subtypes to
-- 'Proarrow.Optic.Fold.Fold' and 'Proarrow.Optic.Setter.Setter'. Build with 'traversed' (from a
-- 'Traversable') or 'Proarrow.Optic.MonoidalTraversal.traversal' (from the van-Laarhoven form),
-- eliminate with 'traverseOf'.
module Proarrow.Optic.Traversal where

import Proarrow.Adjunction (Proadjunction (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Action (CoprodAction, ProdAction)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Category.Monoidal.Distributive
  ( Bicartesian
  , Cotraversable (..)
  , Distributive
  , StrongDistributiveProfunctor
  , Traversable (..)
  , corepTraverse
  , repTraverse
  )
import Proarrow.Category.Monoidal.Strength (Strong (..))
import Proarrow.Colimit.BinaryCoproduct
  ( COPROD (..)
  , Coproduct
  , HasBinaryCoproducts (..)
  , HasCoproducts
  , nil
  , (++)
  )
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (\\), type (+->))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), PROD (..), Product)
import Proarrow.Monoid (Monoid (..))
import Proarrow.Optic
  ( CompactFlavor (..)
  , ExOptic (..)
  , FLAVOR
  , Optic
  , Prostrong (..)
  , SubFlavor (..)
  , convert
  , ex2prof
  , withLegs
  )
import Proarrow.Optic.Fold (FoldRes (..))
import Proarrow.Optic.Setter (SetterRes (..))
import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..), coindex)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (CorepStar (..), Rep (..), RepCostar (..), Representable (..))

type TravRes :: forall {k}. FLAVOR k k
class (SetterRes p q, FoldRes p q) => TravRes (p :: k +-> k) (q :: k +-> k) where
  -- | Distribute a traversal-strength profunctor. Only the product-lens witness genuinely needs
  -- @'Strong' 'ProdAction'@ (to carry the residual through the categorical product); every other
  -- witness distributes a plain 'StrongDistributiveProfunctor' and inherits 'travP' from 'monTravP'.
  travP :: (StrongDistributiveProfunctor r, Strong ProdAction r) => p s a -> q b t -> r a b -> r s t
  default travP :: (MonTravRes p q, StrongDistributiveProfunctor r) => p s a -> q b t -> r a b -> r s t
  travP = p s a -> q b t -> r a b -> r s t
forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
p s a -> q b t -> r a b -> r s t
monTravP

-- | A __monoidal traversal__ sits between 'Proarrow.Optic.Kaleidoscope.Kaleidoscope' and
-- 'Traversal': it distributes any 'StrongDistributiveProfunctor' without the product-strength a
-- lens-as-traversal needs. Every traversal witness except the product lens is a monoidal traversal.
type MonTravRes :: forall {k}. FLAVOR k k
class (TravRes p q) => MonTravRes (p :: k +-> k) (q :: k +-> k) where
  monTravP :: (StrongDistributiveProfunctor r) => p s a -> q b t -> r a b -> r s t

instance (Bicartesian k, Traversable t, Representable t) => TravRes (t :: k +-> k) (RepCostar t)
instance (Bicartesian k, Traversable t, Representable t) => MonTravRes (t :: k +-> k) (RepCostar t) where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
t s a -> RepCostar t b t -> r a b -> r s t
monTravP t s a
l (RepCostar (t % b) ~> t
r) = (s ~> (t % a)) -> ((t % b) ~> t) -> r (t % a) (t % b) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r 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 (t s a -> s ~> (t % a)
forall (a :: k) (b :: k). t a b -> a ~> (t % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index t s a
l) (t % b) ~> t
r (r (t % a) (t % b) -> r s t)
-> (r a b -> r (t % a) (t % b)) -> r a b -> r s t
forall b c a. (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} (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
forall (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
repTraverse @t

-- | The former cotraversal witness: a corepresentable 'Cotraversable' functor builds @s@ from a
-- shape of @a@'s. Its 'travP' distributes an SDP exactly as the old @cotravP@ did -- for these
-- (representable) witnesses a cotraversal /is/ a traversal, which is why there is no separate
-- @Cotraversal@ optic.
instance (Bicartesian k, Cotraversable t, Corepresentable t) => TravRes (CorepStar t) (t :: k +-> k)

instance (Bicartesian k, Cotraversable t, Corepresentable t) => MonTravRes (CorepStar t) (t :: k +-> k) where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
CorepStar t s a -> t b t -> r a b -> r s t
monTravP (CorepStar s ~> (t %% a)
l) t b t
co = (s ~> (t %% a)) -> ((t %% b) ~> t) -> r (t %% a) (t %% b) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r 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 s ~> (t %% a)
l (t b t -> (t %% b) ~> t
forall (a :: k) (b :: k). t a b -> (t %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex t b t
co) (r (t %% a) (t %% b) -> r s t)
-> (r a b -> r (t %% a) (t %% b)) -> r a b -> r s t
forall b c a. (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} (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Cotraversable t, Corepresentable t,
 StrongDistributiveProfunctor p) =>
p a b -> p (t %% a) (t %% b)
forall (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Cotraversable t, Corepresentable t,
 StrongDistributiveProfunctor p) =>
p a b -> p (t %% a) (t %% b)
corepTraverse @t

instance (HasBinaryProducts k, Ob (s :: k)) => TravRes (Rep (Product s)) (Corep (Product s)) where
  travP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
(StrongDistributiveProfunctor r, Strong ProdAction r) =>
Rep (Product s) s a -> Corep (Product s) b t -> r a b -> r s t
travP (Rep s ~> (Product s @ a)
p) (Corep (Product s @ b) ~> t
q) r a b
r = (s ~> (s && a)) -> ((s && b) ~> t) -> r (s && a) (s && b) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r 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 s ~> (Product s @ a)
s ~> (s && a)
p (Product s @ b) ~> t
(s && b) ~> t
q (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 :: (PROD k, k) +-> k) (p :: k +-> k) (a :: PROD k)
       (x :: k) (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @ProdAction @_ @(PR s) r a b
r)
instance (CopyDiscard k, HasCoproducts k, Ob t) => TravRes (Rep (Coproduct t) :: k +-> k) (Corep (Coproduct t))
instance (CopyDiscard k, HasCoproducts k, Ob t) => MonTravRes (Rep (Coproduct t) :: k +-> k) (Corep (Coproduct t)) where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
Rep (Coproduct t) s a -> Corep (Coproduct t) b t -> r a b -> r s t
monTravP (Rep s ~> (Coproduct t @ a)
p) (Corep (Coproduct t @ b) ~> t
q) r a b
r = (s ~> (t || a)) -> ((t || b) ~> t) -> r (t || a) (t || b) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r 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 s ~> (Coproduct t @ a)
s ~> (t || a)
p (Coproduct t @ b) ~> t
(t || b) ~> t
q (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 :: (COPROD k, k) +-> k) (p :: k +-> k) (a :: COPROD k)
       (x :: k) (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @CoprodAction @_ @(COPR t) r a b
r)
instance (CategoryOf k) => TravRes (Id :: k +-> k) (Id :: k +-> k)
instance (CategoryOf k) => MonTravRes (Id :: k +-> k) (Id :: k +-> k) where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
Id s a -> Id b t -> r a b -> r s t
monTravP (Id s ~> a
l) (Id b ~> t
r) = (s ~> a) -> (b ~> t) -> r a b -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r 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 s ~> a
l b ~> t
r
instance (TravRes f g, TravRes f' g') => TravRes (f :.: f') (g' :.: g) where
  travP :: forall (r :: i +-> i) (s :: i) (a :: i) (b :: i) (t :: i).
(StrongDistributiveProfunctor r, Strong ProdAction r) =>
(:.:) f f' s a -> (:.:) g' g b t -> r a b -> r s t
travP (f s b
f :.: f' b a
f') (g' b b
g' :.: g b t
g) = forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: i +-> i) (q :: i +-> i) (r :: i +-> i) (s :: i)
       (a :: i) (b :: i) (t :: i).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP @f @g f s b
f g b t
g (r b b -> r s t) -> (r a b -> r b b) -> r a b -> r s t
forall b c a. (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} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: i +-> i) (q :: i +-> i) (r :: i +-> i) (s :: i)
       (a :: i) (b :: i) (t :: i).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP @f' @g' f' b a
f' g' b b
g'
instance (MonTravRes f g, MonTravRes f' g') => MonTravRes (f :.: f') (g' :.: g) where
  monTravP :: forall (r :: i +-> i) (s :: i) (a :: i) (b :: i) (t :: i).
StrongDistributiveProfunctor r =>
(:.:) f f' s a -> (:.:) g' g b t -> r a b -> r s t
monTravP (f s b
f :.: f' b a
f') (g' b b
g' :.: g b t
g) = forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: i +-> i) (q :: i +-> i) (r :: i +-> i) (s :: i)
       (a :: i) (b :: i) (t :: i).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
monTravP @f @g f s b
f g b t
g (r b b -> r s t) -> (r a b -> r b b) -> r a b -> r s t
forall b c a. (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} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: i +-> i) (q :: i +-> i) (r :: i +-> i) (s :: i)
       (a :: i) (b :: i) (t :: i).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
monTravP @f' @g' f' b a
f' g' b b
g'

instance CompactFlavor TravRes
instance CompactFlavor MonTravRes

instance SubFlavor TravRes SetterRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
TravRes p q =>
(SetterRes p q => r) -> r
subFlavor SetterRes p q => r
r = r
SetterRes p q => r
r
instance SubFlavor TravRes FoldRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
TravRes p q =>
(FoldRes p q => r) -> r
subFlavor FoldRes p q => r
r = r
FoldRes p q => r
r
instance SubFlavor MonTravRes TravRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
MonTravRes p q =>
(TravRes p q => r) -> r
subFlavor TravRes p q => r
r = r
TravRes p q => r
r
instance SubFlavor MonTravRes SetterRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
MonTravRes p q =>
(SetterRes p q => r) -> r
subFlavor SetterRes p q => r
r = r
SetterRes p q => r
r
instance SubFlavor MonTravRes FoldRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
MonTravRes p q =>
(FoldRes p q => r) -> r
subFlavor FoldRes p q => r
r = r
FoldRes p q => r
r

type Traversal (s :: k) (t :: k) a b = Optic (Prostrong TravRes) s t a b
type Traversal' s a = Traversal s s a a

-- | Traverse: distribute any 'StrongDistributiveProfunctor' -- not merely a @Star f@ (the
-- Hask van-Laarhoven shape) -- through any optic that is at least a 'Traversal'. Works for an
-- arbitrary profunctor carrier by handing it to 'travP', rather than relying on a per-carrier
-- @'Prostrong' w p@ bridge (which could only ever cover specific carrier heads).
traverseOf
  :: forall {k} w (s :: k) (t :: k) a b p
   . (Distributive k, StrongDistributiveProfunctor p, Strong ProdAction p, SubFlavor w TravRes)
  => Optic (Prostrong w) s t a b -> p a b -> p s t
traverseOf :: forall {k} (w :: FLAVOR k k) (s :: k) (t :: k) (a :: k) (b :: k)
       (p :: k +-> k).
(Distributive k, StrongDistributiveProfunctor p,
 Strong ProdAction p, SubFlavor w TravRes) =>
Optic (Prostrong w) s t a b -> p a b -> p s t
traverseOf Optic (Prostrong w) s t a b
o p a b
pab = (forall (p :: k +-> k) (q :: k +-> k).
 (TravRes p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> p s t)
-> Optic (Prostrong TravRes) s t a b -> p s t
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs (\p s a
l q b t
r -> p s a -> q b t -> p a b -> p s t
forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
(StrongDistributiveProfunctor r, Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP p s a
l q b t
r p a b
pab) (forall {j} {k} (c :: (k -> j -> Type) -> Constraint)
       (w :: FLAVOR j k) (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b -> Optic (Prostrong w) s t a b
forall (c :: (k +-> k) -> Constraint) (w :: FLAVOR k k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b -> Optic (Prostrong w) s t a b
convert @(Prostrong w) @TravRes Optic (Prostrong w) s t a b
o)

-- | Build a traversal from a 'Traversable' (representable) functor @t@: it focuses every element
-- the functor holds. This is the one weak-flavor builder that is genuinely primitive -- a
-- 'Traversable's traversal is not reachable by 'convert' from any single stronger optic. The
-- witness is @t@ itself paired with @'RepCostar' t@ (see 'TravRes' above); the two legs are the
-- representable universal @'repUniv'@ and the identity 'RepCostar'.
traversed
  :: forall {k} (t :: k +-> k) a b
   . (Bicartesian k, Traversable t, Representable t, Ob a, Ob b) => Traversal (t % a) (t % b) a b
traversed :: forall {k} (t :: k +-> k) (a :: k) (b :: k).
(Bicartesian k, Traversable t, Representable t, Ob a, Ob b) =>
Traversal (t % a) (t % b) a b
traversed = ExOptic TravRes a b (t % a) (t % b)
-> Optic_ (OPT a b) (OPT (t % a) (t % b))
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof (forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(TravRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic TravRes a b) q s t -> ExOptic TravRes a b s t
ExProstrong @t @(RepCostar t) (t (t % a) a
forall (a :: k). Ob a => t (t % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv t (t % a) a
-> ExOptic TravRes a b a b
-> (:.:) t (ExOptic TravRes a b) (t % 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) -> ExOptic TravRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso 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 (:.:) t (ExOptic TravRes a b) (t % a) b
-> RepCostar t b (t % b)
-> (:.:) (t :.: ExOptic TravRes a b) (RepCostar t) (t % a) (t % 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
:.: RepCostar t b (RepCostar t %% b)
RepCostar t b (t % b)
forall (a :: k). Ob a => RepCostar t a (RepCostar t %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv))

-- * The free traversal profunctor

-- | Witness pair for traversing two juxtaposed (tensored) parts in sequence, both parts
-- focusing the same type @x@.
--
-- 'Beside' and 'CoBeside' are each one half of 'Proarrow.Profunctor.Instance.Day.Day' with the
-- two foci types identified -- a one-sided Day convolution, pointwise in the shared focus. The
-- identification is essential: a @('Proarrow.Profunctor.Instance.Day.Day' p1 p2,
-- 'Proarrow.Profunctor.Instance.Day.Day' q1 q2)@ witness pair admits no componentwise 'travP'
-- (that would require splitting a 'StrongDistributiveProfunctor' value at a tensor), which is
-- why 'Proarrow.Optic.Day.DayRes'-flavored optics focus /pairs/ @a1 ** a2@ while these
-- witnesses visit each half's foci in sequence.
type Beside :: forall {k}. (k +-> k) -> (k +-> k) -> k +-> k
data Beside p1 p2 s x where
  Beside :: (s ~> (s1 ** s2)) -> p1 s1 x -> p2 s2 x -> Beside p1 p2 s x

-- | The covariant half of the 'Beside' witness pair: recomposes the two parts' targets,
-- @(t1 '**' t2) '~>' t@.
type CoBeside :: forall {k}. (k +-> k) -> (k +-> k) -> k +-> k
data CoBeside q1 q2 x t where
  CoBeside :: q1 x t1 -> q2 x t2 -> ((t1 ** t2) ~> t) -> CoBeside q1 q2 x t

instance (Profunctor p1, Profunctor p2, Monoidal k) => Profunctor (Beside p1 p2 :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Beside p1 p2 a b -> Beside p1 p2 c d
dimap c ~> a
l b ~> d
r (Beside a ~> (s1 ** s2)
d p1 s1 b
x p2 s2 b
y) = (c ~> (s1 ** s2)) -> p1 s1 d -> p2 s2 d -> Beside p1 p2 c d
forall {k} (s :: k) (t1 :: k) (t2 :: k) (p1 :: k +-> k) (x :: k)
       (p2 :: k +-> k).
(s ~> (t1 ** t2)) -> p1 t1 x -> p2 t2 x -> Beside p1 p2 s x
Beside (a ~> (s1 ** s2)
d (a ~> (s1 ** s2)) -> (c ~> a) -> c ~> (s1 ** s2)
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) ((b ~> d) -> p1 s1 b -> p1 s1 d
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p1 a b -> p1 a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r p1 s1 b
x) ((b ~> d) -> p2 s2 b -> p2 s2 d
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p2 a b -> p2 a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r p2 s2 b
y) ((Ob c, Ob a) => Beside p1 p2 c d) -> (c ~> a) -> Beside p1 p2 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 a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> Beside p1 p2 a b -> r
\\ Beside a ~> (s1 ** s2)
d p1 s1 b
x p2 s2 b
_ = r
(Ob a, Ob b) => r
(Ob a, Ob (s1 ** s2)) => r
r ((Ob a, Ob (s1 ** s2)) => r) -> (a ~> (s1 ** s2)) -> 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 ~> (s1 ** s2)
d ((Ob s1, Ob b) => r) -> p1 s1 b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p1 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
\\ p1 s1 b
x
instance (Profunctor q1, Profunctor q2, Monoidal k) => Profunctor (CoBeside q1 q2 :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> CoBeside q1 q2 a b -> CoBeside q1 q2 c d
dimap c ~> a
l b ~> d
r (CoBeside q1 a t1
u q2 a t2
v (t1 ** t2) ~> b
c) = q1 c t1 -> q2 c t2 -> ((t1 ** t2) ~> d) -> CoBeside q1 q2 c d
forall {k} (q1 :: k +-> k) (x :: k) (t1 :: k) (q2 :: k +-> k)
       (t2 :: k) (t :: k).
q1 x t1 -> q2 x t2 -> ((t1 ** t2) ~> t) -> CoBeside q1 q2 x t
CoBeside ((c ~> a) -> q1 a t1 -> q1 c t1
forall (c :: k) (a :: k) (b :: k). (c ~> a) -> q1 a b -> q1 c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l q1 a t1
u) ((c ~> a) -> q2 a t2 -> q2 c t2
forall (c :: k) (a :: k) (b :: k). (c ~> a) -> q2 a b -> q2 c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l q2 a t2
v) (b ~> d
r (b ~> d) -> ((t1 ** t2) ~> b) -> (t1 ** t2) ~> 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
. (t1 ** t2) ~> b
c) ((Ob b, Ob d) => CoBeside q1 q2 c d)
-> (b ~> d) -> CoBeside q1 q2 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) -> CoBeside q1 q2 a b -> r
\\ CoBeside q1 a t1
u q2 a t2
_ (t1 ** t2) ~> b
c = r
(Ob a, Ob b) => r
(Ob a, Ob t1) => r
r ((Ob a, Ob t1) => r) -> q1 a t1 -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> q1 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
\\ q1 a t1
u ((Ob (t1 ** t2), Ob b) => r) -> ((t1 ** t2) ~> 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
\\ (t1 ** t2) ~> b
c

instance (SetterRes p1 q1, SetterRes p2 q2, Monoidal k) => SetterRes (Beside p1 p2 :: k +-> k) (CoBeside q1 q2) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Beside p1 p2 s a -> CoBeside q1 q2 b t -> (a ~> b) -> s ~> t
overP (Beside s ~> (s1 ** s2)
d p1 s1 a
l1 p2 s2 a
l2) (CoBeside q1 b t1
r1 q2 b t2
r2 (t1 ** t2) ~> t
c) a ~> b
f = (t1 ** t2) ~> t
c ((t1 ** t2) ~> t) -> (s ~> (t1 ** t2)) -> s ~> t
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} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
overP @p1 @q1 p1 s1 a
l1 q1 b t1
r1 a ~> b
f (s1 ~> t1) -> (s2 ~> t2) -> (s1 ** s2) ~> (t1 ** t2)
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} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
overP @p2 @q2 p2 s2 a
l2 q2 b t2
r2 a ~> b
f) ((s1 ** s2) ~> (t1 ** t2)) -> (s ~> (s1 ** s2)) -> s ~> (t1 ** t2)
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
. s ~> (s1 ** s2)
d
instance (FoldRes p1 q1, FoldRes p2 q2, Monoidal k) => FoldRes (Beside p1 p2 :: k +-> k) (CoBeside q1 q2 :: k +-> k) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
Beside p1 p2 s a -> (a ~> m) -> s ~> m
foldMapP (Beside s ~> (s1 ** s2)
d p1 s1 a
l1 p2 s2 a
l2) a ~> m
am = (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend ((m ** m) ~> m) -> (s ~> (m ** m)) -> s ~> m
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 {j} {k} (p :: k +-> k) (q :: j +-> j) (m :: k) (s :: k)
       (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
forall (p :: k +-> k) (q :: k +-> k) (m :: k) (s :: k) (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
foldMapP @p1 @q1 p1 s1 a
l1 a ~> m
am (s1 ~> m) -> (s2 ~> m) -> (s1 ** s2) ~> (m ** m)
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 {j} {k} (p :: k +-> k) (q :: j +-> j) (m :: k) (s :: k)
       (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
forall (p :: k +-> k) (q :: k +-> k) (m :: k) (s :: k) (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
foldMapP @p2 @q2 p2 s2 a
l2 a ~> m
am) ((s1 ** s2) ~> (m ** m)) -> (s ~> (s1 ** s2)) -> s ~> (m ** m)
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
. s ~> (s1 ** s2)
d
instance (TravRes p1 q1, TravRes p2 q2, Monoidal k) => TravRes (Beside p1 p2 :: k +-> k) (CoBeside q1 q2) where
  travP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
(StrongDistributiveProfunctor r, Strong ProdAction r) =>
Beside p1 p2 s a -> CoBeside q1 q2 b t -> r a b -> r s t
travP (Beside s ~> (s1 ** s2)
d p1 s1 a
l1 p2 s2 a
l2) (CoBeside q1 b t1
r1 q2 b t2
r2 (t1 ** t2) ~> t
c) r a b
r = (s ~> (s1 ** s2))
-> ((t1 ** t2) ~> t) -> r (s1 ** s2) (t1 ** t2) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r 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 s ~> (s1 ** s2)
d (t1 ** t2) ~> t
c (forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP @p1 @q1 p1 s1 a
l1 q1 b t1
r1 r a b
r r s1 t1 -> r s2 t2 -> r (s1 ** s2) (t1 ** t2)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
r x1 x2 -> r y1 y2 -> r (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} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP @p2 @q2 p2 s2 a
l2 q2 b t2
r2 r a b
r)
instance (MonTravRes p1 q1, MonTravRes p2 q2, Monoidal k) => MonTravRes (Beside p1 p2 :: k +-> k) (CoBeside q1 q2) where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
Beside p1 p2 s a -> CoBeside q1 q2 b t -> r a b -> r s t
monTravP (Beside s ~> (s1 ** s2)
d p1 s1 a
l1 p2 s2 a
l2) (CoBeside q1 b t1
r1 q2 b t2
r2 (t1 ** t2) ~> t
c) r a b
r = (s ~> (s1 ** s2))
-> ((t1 ** t2) ~> t) -> r (s1 ** s2) (t1 ** t2) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r 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 s ~> (s1 ** s2)
d (t1 ** t2) ~> t
c (forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
monTravP @p1 @q1 p1 s1 a
l1 q1 b t1
r1 r a b
r r s1 t1 -> r s2 t2 -> r (s1 ** s2) (t1 ** t2)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
r x1 x2 -> r y1 y2 -> r (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} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
monTravP @p2 @q2 p2 s2 a
l2 q2 b t2
r2 r a b
r)
instance (Proadjunction p1 q1, Proadjunction p2 q2, Monoidal k) => Proadjunction (Beside p1 p2 :: k +-> k) (CoBeside q1 q2) where
  unit :: forall (a :: k). Ob a => (:.:) (CoBeside q1 q2) (Beside p1 p2) a a
unit @a = case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: k +-> k) (q :: k +-> k) (a :: k).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
unit @p1 @q1 @a of
    (:.:) @m1 q1 a b
u1 p1 b a
v1 -> case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: k +-> k) (q :: k +-> k) (a :: k).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
unit @p2 @q2 @a of
      (:.:) @m2 q2 a b
u2 p2 b a
v2 -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @m1 @m2 (q1 a b
-> q2 a b -> ((b ** b) ~> (b ** b)) -> CoBeside q1 q2 a (b ** b)
forall {k} (q1 :: k +-> k) (x :: k) (t1 :: k) (q2 :: k +-> k)
       (t2 :: k) (t :: k).
q1 x t1 -> q2 x t2 -> ((t1 ** t2) ~> t) -> CoBeside q1 q2 x t
CoBeside q1 a b
u1 q2 a b
u2 (b ** b) ~> (b ** b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id CoBeside q1 q2 a (b ** b)
-> Beside p1 p2 (b ** b) a
-> (:.:) (CoBeside q1 q2) (Beside p1 p2) a a
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) ~> (b ** b))
-> p1 b a -> p2 b a -> Beside p1 p2 (b ** b) a
forall {k} (s :: k) (t1 :: k) (t2 :: k) (p1 :: k +-> k) (x :: k)
       (p2 :: k +-> k).
(s ~> (t1 ** t2)) -> p1 t1 x -> p2 t2 x -> Beside p1 p2 s x
Beside (b ** b) ~> (b ** b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id p1 b a
v1 p2 b a
v2) ((Ob b, Ob a) => (:.:) (CoBeside q1 q2) (Beside p1 p2) a a)
-> p1 b a -> (:.:) (CoBeside q1 q2) (Beside p1 p2) a a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p1 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
\\ p1 b a
v1 ((Ob b, Ob a) => (:.:) (CoBeside q1 q2) (Beside p1 p2) a a)
-> p2 b a -> (:.:) (CoBeside q1 q2) (Beside p1 p2) a a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p2 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
\\ p2 b a
v2
  counit :: (Beside p1 p2 :.: CoBeside q1 q2) :~> (~>)
counit (Beside a ~> (s1 ** s2)
d p1 s1 b
l1 p2 s2 b
l2 :.: CoBeside q1 b t1
r1 q2 b t2
r2 (t1 ** t2) ~> b
c) = (t1 ** t2) ~> b
c ((t1 ** t2) ~> b) -> (a ~> (t1 ** t2)) -> a ~> b
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
. ((:.:) p1 q1 s1 t1 -> s1 ~> t1
(p1 :.: q1) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
counit (p1 s1 b
l1 p1 s1 b -> q1 b t1 -> (:.:) p1 q1 s1 t1
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
:.: q1 b t1
r1) (s1 ~> t1) -> (s2 ~> t2) -> (s1 ** s2) ~> (t1 ** t2)
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)
** (:.:) p2 q2 s2 t2 -> s2 ~> t2
(p2 :.: q2) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
counit (p2 s2 b
l2 p2 s2 b -> q2 b t2 -> (:.:) p2 q2 s2 t2
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
:.: q2 b t2
r2)) ((s1 ** s2) ~> (t1 ** t2)) -> (a ~> (s1 ** s2)) -> a ~> (t1 ** t2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (s1 ** s2)
d

-- | Witness pair for traversing one of two alternative (coproduct) parts: the same one-sided
-- Day convolution as 'Beside'\/'CoBeside', but over the coproduct monoidal structure (cf.
-- 'Proarrow.Colimit.BinaryCoproduct.Coprod').
type BesideSum :: forall {k}. (k +-> k) -> (k +-> k) -> k +-> k
data BesideSum p1 p2 s x where
  BesideSum :: (s ~> (s1 || s2)) -> p1 s1 x -> p2 s2 x -> BesideSum p1 p2 s x

-- | The covariant half of the 'BesideSum' witness pair: recomposes the branches' targets,
-- @(t1 '||' t2) '~>' t@.
type CoBesideSum :: forall {k}. (k +-> k) -> (k +-> k) -> k +-> k
data CoBesideSum q1 q2 x t where
  CoBesideSum :: q1 x t1 -> q2 x t2 -> ((t1 || t2) ~> t) -> CoBesideSum q1 q2 x t

instance (Profunctor p1, Profunctor p2, CategoryOf k) => Profunctor (BesideSum p1 p2 :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> BesideSum p1 p2 a b -> BesideSum p1 p2 c d
dimap c ~> a
l b ~> d
r (BesideSum a ~> (s1 || s2)
d p1 s1 b
x p2 s2 b
y) = (c ~> (s1 || s2)) -> p1 s1 d -> p2 s2 d -> BesideSum p1 p2 c d
forall {k} (s :: k) (t1 :: k) (t2 :: k) (p1 :: k +-> k) (x :: k)
       (p2 :: k +-> k).
(s ~> (t1 || t2)) -> p1 t1 x -> p2 t2 x -> BesideSum p1 p2 s x
BesideSum (a ~> (s1 || s2)
d (a ~> (s1 || s2)) -> (c ~> a) -> c ~> (s1 || s2)
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) ((b ~> d) -> p1 s1 b -> p1 s1 d
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p1 a b -> p1 a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r p1 s1 b
x) ((b ~> d) -> p2 s2 b -> p2 s2 d
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p2 a b -> p2 a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r p2 s2 b
y) ((Ob c, Ob a) => BesideSum p1 p2 c d)
-> (c ~> a) -> BesideSum p1 p2 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 a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> BesideSum p1 p2 a b -> r
\\ BesideSum a ~> (s1 || s2)
d p1 s1 b
x p2 s2 b
_ = r
(Ob a, Ob b) => r
(Ob a, Ob (s1 || s2)) => r
r ((Ob a, Ob (s1 || s2)) => r) -> (a ~> (s1 || s2)) -> 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 ~> (s1 || s2)
d ((Ob s1, Ob b) => r) -> p1 s1 b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p1 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
\\ p1 s1 b
x
instance (Profunctor q1, Profunctor q2, CategoryOf k) => Profunctor (CoBesideSum q1 q2 :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a)
-> (b ~> d) -> CoBesideSum q1 q2 a b -> CoBesideSum q1 q2 c d
dimap c ~> a
l b ~> d
r (CoBesideSum q1 a t1
u q2 a t2
v (t1 || t2) ~> b
c) = q1 c t1 -> q2 c t2 -> ((t1 || t2) ~> d) -> CoBesideSum q1 q2 c d
forall {k} (q1 :: k +-> k) (x :: k) (t1 :: k) (q2 :: k +-> k)
       (t2 :: k) (t :: k).
q1 x t1 -> q2 x t2 -> ((t1 || t2) ~> t) -> CoBesideSum q1 q2 x t
CoBesideSum ((c ~> a) -> q1 a t1 -> q1 c t1
forall (c :: k) (a :: k) (b :: k). (c ~> a) -> q1 a b -> q1 c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l q1 a t1
u) ((c ~> a) -> q2 a t2 -> q2 c t2
forall (c :: k) (a :: k) (b :: k). (c ~> a) -> q2 a b -> q2 c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l q2 a t2
v) (b ~> d
r (b ~> d) -> ((t1 || t2) ~> b) -> (t1 || t2) ~> 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
. (t1 || t2) ~> b
c) ((Ob b, Ob d) => CoBesideSum q1 q2 c d)
-> (b ~> d) -> CoBesideSum q1 q2 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) -> CoBesideSum q1 q2 a b -> r
\\ CoBesideSum q1 a t1
u q2 a t2
_ (t1 || t2) ~> b
c = r
(Ob a, Ob b) => r
(Ob a, Ob t1) => r
r ((Ob a, Ob t1) => r) -> q1 a t1 -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> q1 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
\\ q1 a t1
u ((Ob (t1 || t2), Ob b) => r) -> ((t1 || t2) ~> 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
\\ (t1 || t2) ~> b
c

instance (SetterRes p1 q1, SetterRes p2 q2, HasBinaryCoproducts k) => SetterRes (BesideSum p1 p2 :: k +-> k) (CoBesideSum q1 q2) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
BesideSum p1 p2 s a -> CoBesideSum q1 q2 b t -> (a ~> b) -> s ~> t
overP (BesideSum s ~> (s1 || s2)
d p1 s1 a
l1 p2 s2 a
l2) (CoBesideSum q1 b t1
r1 q2 b t2
r2 (t1 || t2) ~> t
c) a ~> b
f = (t1 || t2) ~> t
c ((t1 || t2) ~> t) -> (s ~> (t1 || t2)) -> s ~> t
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} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
overP @p1 @q1 p1 s1 a
l1 q1 b t1
r1 a ~> b
f (s1 ~> t1) -> (s2 ~> t2) -> (s1 || s2) ~> (t1 || t2)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k).
SetterRes p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
overP @p2 @q2 p2 s2 a
l2 q2 b t2
r2 a ~> b
f) ((s1 || s2) ~> (t1 || t2)) -> (s ~> (s1 || s2)) -> s ~> (t1 || t2)
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
. s ~> (s1 || s2)
d
instance
  (FoldRes p1 q1, FoldRes p2 q2, HasBinaryCoproducts k)
  => FoldRes (BesideSum p1 p2 :: k +-> k) (CoBesideSum q1 q2 :: k +-> k)
  where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
BesideSum p1 p2 s a -> (a ~> m) -> s ~> m
foldMapP (BesideSum s ~> (s1 || s2)
d p1 s1 a
l1 p2 s2 a
l2) a ~> m
am = (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (m :: k) (s :: k)
       (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
forall (p :: k +-> k) (q :: k +-> k) (m :: k) (s :: k) (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
foldMapP @p1 @q1 p1 s1 a
l1 a ~> m
am (s1 ~> m) -> (s2 ~> m) -> (s1 || s2) ~> m
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| forall {j} {k} (p :: k +-> k) (q :: j +-> j) (m :: k) (s :: k)
       (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
forall (p :: k +-> k) (q :: k +-> k) (m :: k) (s :: k) (a :: k).
(FoldRes p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
foldMapP @p2 @q2 p2 s2 a
l2 a ~> m
am) ((s1 || s2) ~> m) -> (s ~> (s1 || s2)) -> s ~> m
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
. s ~> (s1 || s2)
d
instance (TravRes p1 q1, TravRes p2 q2, HasBinaryCoproducts k) => TravRes (BesideSum p1 p2 :: k +-> k) (CoBesideSum q1 q2) where
  travP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
(StrongDistributiveProfunctor r, Strong ProdAction r) =>
BesideSum p1 p2 s a -> CoBesideSum q1 q2 b t -> r a b -> r s t
travP (BesideSum s ~> (s1 || s2)
d p1 s1 a
l1 p2 s2 a
l2) (CoBesideSum q1 b t1
r1 q2 b t2
r2 (t1 || t2) ~> t
c) r a b
r = (s ~> (s1 || s2))
-> ((t1 || t2) ~> t) -> r (s1 || s2) (t1 || t2) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r 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 s ~> (s1 || s2)
d (t1 || t2) ~> t
c (forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP @p1 @q1 p1 s1 a
l1 q1 b t1
r1 r a b
r r s1 t1 -> r s2 t2 -> r (s1 || s2) (t1 || t2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
++ forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP @p2 @q2 p2 s2 a
l2 q2 b t2
r2 r a b
r)
instance
  (MonTravRes p1 q1, MonTravRes p2 q2, HasBinaryCoproducts k)
  => MonTravRes (BesideSum p1 p2 :: k +-> k) (CoBesideSum q1 q2)
  where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
BesideSum p1 p2 s a -> CoBesideSum q1 q2 b t -> r a b -> r s t
monTravP (BesideSum s ~> (s1 || s2)
d p1 s1 a
l1 p2 s2 a
l2) (CoBesideSum q1 b t1
r1 q2 b t2
r2 (t1 || t2) ~> t
c) r a b
r = (s ~> (s1 || s2))
-> ((t1 || t2) ~> t) -> r (s1 || s2) (t1 || t2) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r 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 s ~> (s1 || s2)
d (t1 || t2) ~> t
c (forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
monTravP @p1 @q1 p1 s1 a
l1 q1 b t1
r1 r a b
r r s1 t1 -> r s2 t2 -> r (s1 || s2) (t1 || t2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
++ forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
monTravP @p2 @q2 p2 s2 a
l2 q2 b t2
r2 r a b
r)
instance
  (Proadjunction p1 q1, Proadjunction p2 q2, HasBinaryCoproducts k)
  => Proadjunction (BesideSum p1 p2 :: k +-> k) (CoBesideSum q1 q2)
  where
  unit :: forall (a :: k).
Ob a =>
(:.:) (CoBesideSum q1 q2) (BesideSum p1 p2) a a
unit @a = case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: k +-> k) (q :: k +-> k) (a :: k).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
unit @p1 @q1 @a of
    (:.:) @m1 q1 a b
u1 p1 b a
v1 -> case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: k +-> k) (q :: k +-> k) (a :: k).
(Proadjunction p q, Ob a) =>
(:.:) q p a a
unit @p2 @q2 @a of
      (:.:) @m2 q2 a b
u2 p2 b a
v2 -> forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @m1 @m2 (q1 a b
-> q2 a b -> ((b || b) ~> (b || b)) -> CoBesideSum q1 q2 a (b || b)
forall {k} (q1 :: k +-> k) (x :: k) (t1 :: k) (q2 :: k +-> k)
       (t2 :: k) (t :: k).
q1 x t1 -> q2 x t2 -> ((t1 || t2) ~> t) -> CoBesideSum q1 q2 x t
CoBesideSum q1 a b
u1 q2 a b
u2 (b || b) ~> (b || b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id CoBesideSum q1 q2 a (b || b)
-> BesideSum p1 p2 (b || b) a
-> (:.:) (CoBesideSum q1 q2) (BesideSum p1 p2) a a
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) ~> (b || b))
-> p1 b a -> p2 b a -> BesideSum p1 p2 (b || b) a
forall {k} (s :: k) (t1 :: k) (t2 :: k) (p1 :: k +-> k) (x :: k)
       (p2 :: k +-> k).
(s ~> (t1 || t2)) -> p1 t1 x -> p2 t2 x -> BesideSum p1 p2 s x
BesideSum (b || b) ~> (b || b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id p1 b a
v1 p2 b a
v2) ((Ob b, Ob a) => (:.:) (CoBesideSum q1 q2) (BesideSum p1 p2) a a)
-> p1 b a -> (:.:) (CoBesideSum q1 q2) (BesideSum p1 p2) a a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p1 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
\\ p1 b a
v1 ((Ob b, Ob a) => (:.:) (CoBesideSum q1 q2) (BesideSum p1 p2) a a)
-> p2 b a -> (:.:) (CoBesideSum q1 q2) (BesideSum p1 p2) a a
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p2 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
\\ p2 b a
v2
  counit :: (BesideSum p1 p2 :.: CoBesideSum q1 q2) :~> (~>)
counit (BesideSum a ~> (s1 || s2)
d p1 s1 b
l1 p2 s2 b
l2 :.: CoBesideSum q1 b t1
r1 q2 b t2
r2 (t1 || t2) ~> b
c) = (t1 || t2) ~> b
c ((t1 || t2) ~> b) -> (a ~> (t1 || t2)) -> a ~> b
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
. ((:.:) p1 q1 s1 t1 -> s1 ~> t1
(p1 :.: q1) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
counit (p1 s1 b
l1 p1 s1 b -> q1 b t1 -> (:.:) p1 q1 s1 t1
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
:.: q1 b t1
r1) (s1 ~> t1) -> (s2 ~> t2) -> (s1 || s2) ~> (t1 || t2)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ (:.:) p2 q2 s2 t2 -> s2 ~> t2
(p2 :.: q2) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Proadjunction p q =>
(p :.: q) :~> (~>)
counit (p2 s2 b
l2 p2 s2 b -> q2 b t2 -> (:.:) p2 q2 s2 t2
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
:.: q2 b t2
r2)) ((s1 || s2) ~> (t1 || t2)) -> (a ~> (s1 || s2)) -> a ~> (t1 || t2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (s1 || s2)
d

-- | Witness pair with no foci at all: decompose to 'Unit' and rebuild.
--
-- 'UnitW' and 'CoUnitW' are the two halves of 'Proarrow.Profunctor.Instance.Day.DayUnit', one
-- per side of the witness pair, with a phantom focus: together with 'Beside'\/'CoBeside' being
-- the halves of 'Proarrow.Profunctor.Instance.Day.Day', the witness pairs here are exactly the
-- Day-monoidal structure on profunctors (@'Proarrow.Category.Monoidal.Monoidal' (j '+->' k)@),
-- split at the focus. The split is forced: a whole 'Proarrow.Profunctor.Instance.Day.DayUnit'
-- on the decomposition side would demand @Unit ~> a@ for an arbitrary focus @a@.
type UnitW :: forall {k}. k +-> k
data UnitW s x where
  UnitW :: (Ob x) => (s ~> Unit) -> UnitW s x

-- | The covariant half of the 'UnitW' witness pair: rebuilds the target from 'Unit'.
type CoUnitW :: forall {k}. k +-> k
data CoUnitW x t where
  CoUnitW :: (Ob x) => (Unit ~> t) -> CoUnitW x t

instance (Monoidal k) => Profunctor (UnitW :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> UnitW a b -> UnitW c d
dimap c ~> a
l b ~> d
r (UnitW a ~> Unit
h) = (c ~> Unit) -> UnitW c d
forall {k} (x :: k) (s :: k). Ob x => (s ~> Unit) -> UnitW s x
UnitW (a ~> Unit
h (a ~> Unit) -> (c ~> a) -> c ~> 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
. c ~> a
l) ((Ob b, Ob d) => UnitW c d) -> (b ~> d) -> UnitW 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) -> UnitW a b -> r
\\ UnitW a ~> Unit
h = r
(Ob a, Ob b) => r
(Ob a, Ob Unit) => r
r ((Ob a, Ob Unit) => r) -> (a ~> Unit) -> 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 ~> Unit
h
instance (Monoidal k) => Profunctor (CoUnitW :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> CoUnitW a b -> CoUnitW c d
dimap c ~> a
l b ~> d
r (CoUnitW Unit ~> b
i) = (Unit ~> d) -> CoUnitW c d
forall {k} (x :: k) (t :: k). Ob x => (Unit ~> t) -> CoUnitW x t
CoUnitW (b ~> d
r (b ~> d) -> (Unit ~> b) -> Unit ~> 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
. Unit ~> b
i) ((Ob c, Ob a) => CoUnitW c d) -> (c ~> a) -> CoUnitW 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 a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> CoUnitW a b -> r
\\ CoUnitW Unit ~> b
i = r
(Ob a, Ob b) => r
(Ob Unit, Ob b) => r
r ((Ob Unit, Ob b) => r) -> (Unit ~> 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
\\ Unit ~> b
i

instance (Monoidal k) => SetterRes (UnitW :: k +-> k) CoUnitW where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
UnitW s a -> CoUnitW b t -> (a ~> b) -> s ~> t
overP (UnitW s ~> Unit
h) (CoUnitW Unit ~> t
i) a ~> b
_ = Unit ~> t
i (Unit ~> t) -> (s ~> Unit) -> s ~> t
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
. s ~> Unit
h
instance (Monoidal k) => FoldRes (UnitW :: k +-> k) (CoUnitW :: k +-> k) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
UnitW s a -> (a ~> m) -> s ~> m
foldMapP (UnitW s ~> Unit
h) a ~> m
_ = Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty (Unit ~> m) -> (s ~> Unit) -> s ~> m
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
. s ~> Unit
h
instance (Monoidal k) => TravRes (UnitW :: k +-> k) CoUnitW
instance (Monoidal k) => MonTravRes (UnitW :: k +-> k) CoUnitW where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
UnitW s a -> CoUnitW b t -> r a b -> r s t
monTravP (UnitW s ~> Unit
h) (CoUnitW Unit ~> t
i) r a b
_ = (s ~> Unit) -> (Unit ~> t) -> r Unit Unit -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r 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 s ~> Unit
h Unit ~> t
i r Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
instance (Monoidal k) => Proadjunction (UnitW :: k +-> k) CoUnitW where
  unit :: forall (a :: k). Ob a => (:.:) CoUnitW UnitW a a
unit = (Unit ~> Unit) -> CoUnitW a Unit
forall {k} (x :: k) (t :: k). Ob x => (Unit ~> t) -> CoUnitW x t
CoUnitW Unit ~> Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id CoUnitW a Unit -> UnitW Unit a -> (:.:) CoUnitW UnitW a a
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
:.: (Unit ~> Unit) -> UnitW Unit a
forall {k} (x :: k) (s :: k). Ob x => (s ~> Unit) -> UnitW s x
UnitW Unit ~> Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  counit :: (UnitW :.: CoUnitW) :~> (~>)
counit (UnitW a ~> Unit
h :.: CoUnitW Unit ~> b
i) = Unit ~> b
i (Unit ~> b) -> (a ~> Unit) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Unit
h

-- | Witness pair for the impossible case: decompose to the initial object -- the halves of the
-- (unspelled) unit of Day convolution over the coproduct monoidal structure, cf.
-- 'UnitW'\/'CoUnitW'.
type ZeroW :: forall {k}. k +-> k
data ZeroW s x where
  ZeroW :: (Ob x) => (s ~> InitialObject) -> ZeroW s x

-- | The covariant half of the 'ZeroW' witness pair: rebuilds the target from 'InitialObject'.
type CoZeroW :: forall {k}. k +-> k
data CoZeroW x t where
  CoZeroW :: (Ob x) => (InitialObject ~> t) -> CoZeroW x t

instance (HasInitialObject k) => Profunctor (ZeroW :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> ZeroW a b -> ZeroW c d
dimap c ~> a
l b ~> d
r (ZeroW a ~> InitialObject
h) = (c ~> InitialObject) -> ZeroW c d
forall {k} (x :: k) (s :: k).
Ob x =>
(s ~> InitialObject) -> ZeroW s x
ZeroW (a ~> InitialObject
h (a ~> InitialObject) -> (c ~> a) -> c ~> InitialObject
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) ((Ob b, Ob d) => ZeroW c d) -> (b ~> d) -> ZeroW 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) -> ZeroW a b -> r
\\ ZeroW a ~> InitialObject
h = r
(Ob a, Ob b) => r
(Ob a, Ob InitialObject) => r
r ((Ob a, Ob InitialObject) => r) -> (a ~> InitialObject) -> 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 ~> InitialObject
h
instance (HasInitialObject k) => Profunctor (CoZeroW :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> CoZeroW a b -> CoZeroW c d
dimap c ~> a
l b ~> d
r (CoZeroW InitialObject ~> b
i) = (InitialObject ~> d) -> CoZeroW c d
forall {k} (x :: k) (t :: k).
Ob x =>
(InitialObject ~> t) -> CoZeroW x t
CoZeroW (b ~> d
r (b ~> d) -> (InitialObject ~> b) -> InitialObject ~> 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
. InitialObject ~> b
i) ((Ob c, Ob a) => CoZeroW c d) -> (c ~> a) -> CoZeroW 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 a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> CoZeroW a b -> r
\\ CoZeroW InitialObject ~> b
i = r
(Ob a, Ob b) => r
(Ob InitialObject, Ob b) => r
r ((Ob InitialObject, Ob b) => r) -> (InitialObject ~> 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
\\ InitialObject ~> b
i

instance (HasInitialObject k) => SetterRes (ZeroW :: k +-> k) CoZeroW where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
ZeroW s a -> CoZeroW b t -> (a ~> b) -> s ~> t
overP (ZeroW s ~> InitialObject
h) (CoZeroW InitialObject ~> t
i) a ~> b
_ = InitialObject ~> t
i (InitialObject ~> t) -> (s ~> InitialObject) -> s ~> t
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
. s ~> InitialObject
h
instance (HasInitialObject k) => FoldRes (ZeroW :: k +-> k) (CoZeroW :: k +-> k) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
ZeroW s a -> (a ~> m) -> s ~> m
foldMapP (ZeroW s ~> InitialObject
h) a ~> m
_ = InitialObject ~> m
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate (InitialObject ~> m) -> (s ~> InitialObject) -> s ~> m
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
. s ~> InitialObject
h
instance (HasInitialObject k) => TravRes (ZeroW :: k +-> k) CoZeroW
instance (HasInitialObject k) => MonTravRes (ZeroW :: k +-> k) CoZeroW where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
ZeroW s a -> CoZeroW b t -> r a b -> r s t
monTravP (ZeroW s ~> InitialObject
h) (CoZeroW InitialObject ~> t
i) r a b
_ = (s ~> InitialObject)
-> (InitialObject ~> t) -> r InitialObject InitialObject -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r 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 s ~> InitialObject
h InitialObject ~> t
i r InitialObject InitialObject
forall {j} {k} (p :: j +-> k).
MonoidalProfunctor (Coprod p) =>
p InitialObject InitialObject
nil
instance (HasInitialObject k) => Proadjunction (ZeroW :: k +-> k) CoZeroW where
  unit :: forall (a :: k). Ob a => (:.:) CoZeroW ZeroW a a
unit = (InitialObject ~> InitialObject) -> CoZeroW a InitialObject
forall {k} (x :: k) (t :: k).
Ob x =>
(InitialObject ~> t) -> CoZeroW x t
CoZeroW InitialObject ~> InitialObject
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id CoZeroW a InitialObject
-> ZeroW InitialObject a -> (:.:) CoZeroW ZeroW a a
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
:.: (InitialObject ~> InitialObject) -> ZeroW InitialObject a
forall {k} (x :: k) (s :: k).
Ob x =>
(s ~> InitialObject) -> ZeroW s x
ZeroW InitialObject ~> InitialObject
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  counit :: (ZeroW :.: CoZeroW) :~> (~>)
counit (ZeroW a ~> InitialObject
h :.: CoZeroW InitialObject ~> b
i) = InitialObject ~> b
i (InitialObject ~> b) -> (a ~> InitialObject) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> InitialObject
h