{-# 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 'TravFl'\/'MonTravFl' 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'), 'fromTravVL' (from a Prelude traversal) or
-- 'Proarrow.Optic.MonoidalTraversal.traversal' (from the profunctor-class form), eliminate with
-- 'traverseOf'.
module Proarrow.Optic.Traversal where

import Data.Functor.Compose (Compose (..))
import Data.Functor.Const (Const (..))
import Data.Functor.Identity (Identity (..))
import Data.Kind (Type)
import Prelude qualified as P

import Proarrow.Adjunction (Proadjunction (..))
import Proarrow.Category.Instance.Product (Diag, (:**:) (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), MultRep, Tensor)
import Proarrow.Category.Monoidal.Action (ActionAt, CoprodAction, ProdAction)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Category.Monoidal.Distributive
  ( Cotraversable (..)
  , Distributive
  , StrongDistributiveProfunctor
  , Traversable (..)
  , corepTraverse
  , repTraverse
  )
import Proarrow.Category.Monoidal.Strength (Strong (..))
import Proarrow.Colimit.BinaryCoproduct
  ( COPROD (..)
  , Coproduct
  , HasBinaryCoproducts (..)
  , HasCoproducts
  , PlusRep
  , nil
  , (++)
  )
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (\\), type (+->))
import Proarrow.Functor (Prelude (..))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), PROD (..), Product)
import Proarrow.Monoid (Comonoid, Monoid (..))
import Proarrow.Monoid qualified as Mon
import Proarrow.Optic
  ( ExOptic
  , FLAVOR
  , Optic
  , Prostrong (..)
  , legs2prof
  , withLegs
  )
import Proarrow.Optic.Fold (FoldFl (..))
import Proarrow.Optic.Setter (SetterFl (..))
import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..), coindex)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Star (Star, pattern Star)
import Proarrow.Profunctor.Representable (CorepStar (..), Rep (..), RepCostar (..), Representable (..))

type TravFl :: forall {k}. FLAVOR k k
class (SetterFl p q, FoldFl p q) => TravFl (p :: k +-> k) (q :: k +-> k) where
  -- | Distribute a traversal-strength profunctor. Only the product-lens witness 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 :: (MonTravFl 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).
(MonTravFl 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.PowerGrate.PowerGrate' 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 MonTravFl :: forall {k}. FLAVOR k k
class (TravFl p q) => MonTravFl (p :: k +-> k) (q :: k +-> k) where
  monTravP :: (StrongDistributiveProfunctor r) => p s a -> q b t -> r a b -> r s t

instance (Distributive k, CopyDiscard k, Traversable t, Representable t) => TravFl (t :: k +-> k) (RepCostar t)
instance (Distributive k, CopyDiscard k, Traversable t, Representable t) => MonTravFl (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 :: CAT 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, Traversing p) =>
p a b -> p (t % a) (t % b)
forall (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, Traversing p) =>
p a b -> p (t % a) (t % b)
repTraverse @t

-- | A corepresentable 'Cotraversable' functor builds @s@ from a shape of @a@'s, and its 'travP'
-- distributes an SDP the same way a cotraversal's would. So at this witness a cotraversal is a
-- traversal, and it needs no flavor of its own.
-- ("Proarrow.Optic.Kaleidoscope" does define a @Cotraversal@, over 'Cotraversable' witnesses that
-- are not representable. In the lattice it is a sibling of 'Traversal', not a descendant: both are
-- children of @Setter@, and @Cotraversal@\'s own child is @Kaleidoscope@.)
instance (Distributive k, CopyDiscard k, Cotraversable t, Corepresentable t) => TravFl (CorepStar t) (t :: k +-> k)

instance (Distributive k, CopyDiscard k, Cotraversable t, Corepresentable t) => MonTravFl (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 :: CAT 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, Traversing p) =>
p a b -> p (t %% a) (t %% b)
forall (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Cotraversable t, Corepresentable t, Traversing p) =>
p a b -> p (t %% a) (t %% b)
corepTraverse @t

instance (HasBinaryProducts k, Ob (s :: k)) => TravFl (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)

-- | The tensor-action witness pair @'Rep'@\/@'Corep'@ @('ActionAt' 'Tensor' m)@ with a __comonoid__
-- residual @m@ (legs @s ~> m ** a@, @m ** b ~> t@) is a (monoidal) traversal witness. It folds by
-- discarding the residual with the counit, and distributes a 'StrongDistributiveProfunctor' by its
-- own strength @'act' \@'Tensor'@, so neither product strength nor @tensor = product@ is needed.
-- Only @m@ must be a 'Comonoid', so this works in @LINEAR@ for the duplicable objects. It is also
-- the monoidal-lens witness ("Proarrow.Optic.MonoidalLens").
instance (Comonoid (m :: k)) => FoldFl (Rep (ActionAt Tensor m) :: k +-> k) (Corep (ActionAt Tensor m)) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
Rep (ActionAt Tensor m) s a -> (a ~> m) -> s ~> m
foldMapP (Rep s ~> (ActionAt Tensor m @ a)
h) a ~> m
am = (Unit ** m) ~> m
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((Unit ** m) ~> m) -> (s ~> (Unit ** m)) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
Mon.counit @m (m ~> Unit) -> (a ~> m) -> (m ** a) ~> (Unit ** 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)
** a ~> m
am) ((m ** a) ~> (Unit ** m)) -> (s ~> (m ** a)) -> s ~> (Unit ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (ActionAt Tensor m @ a)
s ~> (m ** a)
h

instance (Comonoid (m :: k)) => TravFl (Rep (ActionAt Tensor m) :: k +-> k) (Corep (ActionAt Tensor m))
instance (Comonoid (m :: k)) => MonTravFl (Rep (ActionAt Tensor m) :: k +-> k) (Corep (ActionAt Tensor m)) where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
Rep (ActionAt Tensor m) s a
-> Corep (ActionAt Tensor m) b t -> r a b -> r s t
monTravP (Rep s ~> (ActionAt Tensor m @ a)
h) (Corep (ActionAt Tensor m @ b) ~> t
i) r a b
r = (s ~> (m ** a)) -> ((m ** b) ~> t) -> r (m ** a) (m ** 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 ~> (ActionAt Tensor m @ a)
s ~> (m ** a)
h (ActionAt Tensor m @ b) ~> t
(m ** b) ~> t
i (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 :: (k, k) +-> k) (p :: k +-> k) (a :: k) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @Tensor @_ @m r a b
r)
instance (CopyDiscard k, HasCoproducts k, Ob t) => TravFl (Rep (Coproduct t) :: k +-> k) (Corep (Coproduct t))
instance (CopyDiscard k, HasCoproducts k, Ob t) => MonTravFl (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) => TravFl (Id :: k +-> k) (Id :: k +-> k)
instance (CategoryOf k) => MonTravFl (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 (TravFl f g, TravFl f' g') => TravFl (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).
(TravFl 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).
(TravFl 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 :: CAT 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).
(TravFl 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).
(TravFl 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 (MonTravFl f g, MonTravFl f' g') => MonTravFl (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).
(MonTravFl 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).
(MonTravFl 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 :: CAT 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).
(MonTravFl 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).
(MonTravFl 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'

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

-- | An applicative Haskell effect absorbs traversal witnesses through 'travP'.
instance (P.Applicative f) => Prostrong TravFl (Star (Prelude f)) where
  proact :: forall (f :: Type +-> Type) (g :: Type +-> Type).
(TravFl f g, Profunctor f, Profunctor g) =>
((f :.: Star (Prelude f)) :.: g) :~> Star (Prelude f)
proact (f a b
p :.: Star (Prelude f) b b
r :.: g b b
q) = f a b
-> g b b -> Star (Prelude f) b b -> Star' ('NT (Prelude f)) a b
forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravFl p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: Type +-> Type) s a b t.
(StrongDistributiveProfunctor r, Strong ProdAction r) =>
f s a -> g b t -> r a b -> r s t
travP f a b
p g b b
q Star (Prelude f) b b
r

-- | Distribute any 'StrongDistributiveProfunctor' (not only a @Star f@, the van-Laarhoven shape)
-- through any optic that is at least a 'Traversal', by handing it to 'travP'.
--
-- The optic may be in any encoding: the constraint asks its class to hold for the generic carrier
-- @'ExOptic' 'TravFl' a b@. A 'Prostrong'-flavored optic discharges it via
-- @forall p q. w p q => 'Proarrow.Optic.Sub' 'TravFl' p q@, a '(%)'-composite one conjunct at a
-- time, and a profunctor-class one ('Proarrow.Optic.MonoidalTraversal.PTraversalFull') through the
-- carrier's by-generator instances.
traverseOf
  :: forall {k} c (s :: k) (t :: k) a b p
   . (Distributive k, StrongDistributiveProfunctor p, Strong ProdAction p, (Ob a, Ob b) => c (ExOptic TravFl a b))
  => Optic c s t a b -> p a b -> p s t
traverseOf :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) (p :: k -> k -> Type).
(Distributive k, StrongDistributiveProfunctor p,
 Strong ProdAction p, (Ob a, Ob b) => c (ExOptic TravFl a b)) =>
Optic c s t a b -> p a b -> p s t
traverseOf Optic c s t a b
o p a b
pab = forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR k k) (c :: (k +-> k) -> Constraint) (s :: k)
       (t :: k) (a :: k) (b :: k) r.
(CategoryOf k, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: k +-> k).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @TravFl Optic c s t a b
o \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).
(TravFl 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

-- | 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 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 'TravFl' above). The two legs are the
-- representable universal @'repUniv'@ and the identity 'RepCostar'.
traversed
  :: forall {k} (t :: k +-> k) a b
   . (Distributive k, CopyDiscard 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).
(Distributive k, CopyDiscard k, Traversable t, Representable t,
 Ob a, Ob b) =>
Traversal (t % a) (t % b) a b
traversed = forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR k k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @TravFl (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k +-> k) (a :: k).
(Representable p, Ob a) =>
p (p % a) a
repUniv @t) (forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: k +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv @(RepCostar t))

-- * The free traversal profunctor

-- | Witness pair for traversing two juxtaposed (tensored) parts in sequence, both focusing @x@:
--
-- > Beside p1 p2 s x = exists s1 s2. (s ~> s1 ** s2, p1 s1 x, p2 s2 x)
--
-- spelled as a composite through @(k, k)@: split the source with the tensor (@'Rep' 'MultRep'@),
-- run the witnesses side by side (':**:'), and identify the foci with the diagonal (@'Rep' 'Diag'@).
-- 'Proarrow.Profunctor.Instance.Day.Day' is the same composite with @'Corep' 'MultRep'@ in place of
-- the diagonal, tensoring the foci instead. Identifying them is necessary: a Day witness pair admits
-- no componentwise 'travP', which would have to split a 'StrongDistributiveProfunctor' value at a
-- tensor. So 'Proarrow.Optic.Day.DayFl' optics focus pairs, while this one visits both foci in turn.
type Beside :: forall {k}. (k +-> k) -> (k +-> k) -> k +-> k
type Beside p1 p2 = Rep MultRep :.: (p1 :**: p2) :.: Rep Diag

-- | The covariant half of the 'Beside' witness pair: duplicate the focus with the diagonal
-- (@'Corep' 'Diag'@), run the two witnesses side by side, recompose the targets with the tensor
-- (@'Corep' 'MultRep'@, @t1 ** t2 ~> t@).
type CoBeside :: forall {k}. (k +-> k) -> (k +-> k) -> k +-> k
type CoBeside q1 q2 = Corep Diag :.: (q1 :**: q2) :.: Corep MultRep

instance (SetterFl p1 q1, SetterFl p2 q2, Monoidal k) => SetterFl (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 (Rep s ~> (MultRep @ b)
d :.: (p1 a1 b1
l1 :**: p2 a2 b2
l2) :.: Rep (a1 ~> b1
f1 :**: a2 ~> b2
f2)) (Corep (a1 ~> b1
g1 :**: a2 ~> b2
g2) :.: (q1 a1 b1
r1 :**: q2 a2 b2
r2) :.: Corep (MultRep @ b) ~> t
c) a ~> b
f =
    (MultRep @ b) ~> t
(b1 ** b2) ~> t
c ((b1 ** b2) ~> t) -> (s ~> (b1 ** b2)) -> s ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT 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).
SetterFl 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).
SetterFl p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
overP @p1 @q1 ((b1 ~> a) -> p1 a1 b1 -> p1 a1 a
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 b1 ~> a
a1 ~> b1
f1 p1 a1 b1
l1) ((b ~> a1) -> q1 a1 b1 -> q1 b b1
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 b ~> a1
a1 ~> b1
g1 q1 a1 b1
r1) a ~> b
f ((Fst @ b) ~> b1)
-> ((Snd @ b) ~> b2) -> ((Fst @ b) ** (Snd @ b)) ~> (b1 ** b2)
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).
SetterFl 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).
SetterFl p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
overP @p2 @q2 ((b2 ~> a) -> p2 a2 b2 -> p2 a2 a
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 b2 ~> a
a2 ~> b2
f2 p2 a2 b2
l2) ((b ~> a2) -> q2 a2 b2 -> q2 b b2
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 b ~> a2
a2 ~> b2
g2 q2 a2 b2
r2) a ~> b
f) (((Fst @ b) ** (Snd @ b)) ~> (b1 ** b2))
-> (s ~> ((Fst @ b) ** (Snd @ b))) -> s ~> (b1 ** b2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (MultRep @ b)
s ~> ((Fst @ b) ** (Snd @ b))
d
instance (FoldFl p1 q1, FoldFl p2 q2, Monoidal k) => FoldFl (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 (Rep s ~> (MultRep @ b)
d :.: (p1 a1 b1
l1 :**: p2 a2 b2
l2) :.: Rep (a1 ~> b1
f1 :**: a2 ~> b2
f2)) 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 :: CAT 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).
(FoldFl p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
forall (p :: k +-> k) (q :: k +-> k) (m :: k) (s :: k) (a :: k).
(FoldFl p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
foldMapP @p1 @q1 ((b1 ~> a) -> p1 a1 b1 -> p1 a1 a
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 b1 ~> a
a1 ~> b1
f1 p1 a1 b1
l1) a ~> m
am ((Fst @ b) ~> m)
-> ((Snd @ b) ~> m) -> ((Fst @ b) ** (Snd @ b)) ~> (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).
(FoldFl p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
forall (p :: k +-> k) (q :: k +-> k) (m :: k) (s :: k) (a :: k).
(FoldFl p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
foldMapP @p2 @q2 ((b2 ~> a) -> p2 a2 b2 -> p2 a2 a
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 b2 ~> a
a2 ~> b2
f2 p2 a2 b2
l2) a ~> m
am) (((Fst @ b) ** (Snd @ b)) ~> (m ** m))
-> (s ~> ((Fst @ b) ** (Snd @ b))) -> s ~> (m ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (MultRep @ b)
s ~> ((Fst @ b) ** (Snd @ b))
d
instance (TravFl p1 q1, TravFl p2 q2, Monoidal k) => TravFl (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 (Rep s ~> (MultRep @ b)
d :.: (p1 a1 b1
l1 :**: p2 a2 b2
l2) :.: Rep (a1 ~> b1
f1 :**: a2 ~> b2
f2)) (Corep (a1 ~> b1
g1 :**: a2 ~> b2
g2) :.: (q1 a1 b1
r1 :**: q2 a2 b2
r2) :.: Corep (MultRep @ b) ~> t
c) r a b
r =
    (s ~> ((Fst @ b) ** (Snd @ b)))
-> ((b1 ** b2) ~> t)
-> r ((Fst @ b) ** (Snd @ b)) (b1 ** b2)
-> 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 ~> (MultRep @ b)
s ~> ((Fst @ b) ** (Snd @ b))
d (MultRep @ b) ~> t
(b1 ** b2) ~> t
c (forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravFl 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).
(TravFl p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP @p1 @q1 ((b1 ~> a) -> p1 a1 b1 -> p1 a1 a
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 b1 ~> a
a1 ~> b1
f1 p1 a1 b1
l1) ((b ~> a1) -> q1 a1 b1 -> q1 b b1
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 b ~> a1
a1 ~> b1
g1 q1 a1 b1
r1) r a b
r r a1 b1 -> r a2 b2 -> r (a1 ** a2) (b1 ** b2)
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).
(TravFl 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).
(TravFl p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP @p2 @q2 ((b2 ~> a) -> p2 a2 b2 -> p2 a2 a
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 b2 ~> a
a2 ~> b2
f2 p2 a2 b2
l2) ((b ~> a2) -> q2 a2 b2 -> q2 b b2
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 b ~> a2
a2 ~> b2
g2 q2 a2 b2
r2) r a b
r)
instance (MonTravFl p1 q1, MonTravFl p2 q2, Monoidal k) => MonTravFl (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 (Rep s ~> (MultRep @ b)
d :.: (p1 a1 b1
l1 :**: p2 a2 b2
l2) :.: Rep (a1 ~> b1
f1 :**: a2 ~> b2
f2)) (Corep (a1 ~> b1
g1 :**: a2 ~> b2
g2) :.: (q1 a1 b1
r1 :**: q2 a2 b2
r2) :.: Corep (MultRep @ b) ~> t
c) r a b
r =
    (s ~> ((Fst @ b) ** (Snd @ b)))
-> ((b1 ** b2) ~> t)
-> r ((Fst @ b) ** (Snd @ b)) (b1 ** b2)
-> 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 ~> (MultRep @ b)
s ~> ((Fst @ b) ** (Snd @ b))
d (MultRep @ b) ~> t
(b1 ** b2) ~> t
c (forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravFl 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).
(MonTravFl p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
monTravP @p1 @q1 ((b1 ~> a) -> p1 a1 b1 -> p1 a1 a
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 b1 ~> a
a1 ~> b1
f1 p1 a1 b1
l1) ((b ~> a1) -> q1 a1 b1 -> q1 b b1
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 b ~> a1
a1 ~> b1
g1 q1 a1 b1
r1) r a b
r r a1 b1 -> r a2 b2 -> r (a1 ** a2) (b1 ** b2)
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).
(MonTravFl 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).
(MonTravFl p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
monTravP @p2 @q2 ((b2 ~> a) -> p2 a2 b2 -> p2 a2 a
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 b2 ~> a
a2 ~> b2
f2 p2 a2 b2
l2) ((b ~> a2) -> q2 a2 b2 -> q2 b b2
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 b ~> a2
a2 ~> b2
g2 q2 a2 b2
r2) r a b
r)

-- | Witness pair for traversing one of two alternative (coproduct) parts: 'Beside' with the tensor
-- replaced by the coproduct (@'Rep' 'PlusRep'@, @s ~> s1 || s2@, and @'Corep' 'PlusRep'@,
-- @t1 || t2 ~> t@). Here identifying the foci and tensoring them agree, since @x1 || x2 ~> x@ is a
-- pair @(x1 ~> x, x2 ~> x)@. So this is Day convolution over the coproduct.
type BesideSum :: forall {k}. (k +-> k) -> (k +-> k) -> k +-> k
type BesideSum p1 p2 = Rep PlusRep :.: (p1 :**: p2) :.: Rep Diag

-- | The covariant half of the 'BesideSum' witness pair.
type CoBesideSum :: forall {k}. (k +-> k) -> (k +-> k) -> k +-> k
type CoBesideSum q1 q2 = Corep Diag :.: (q1 :**: q2) :.: Corep PlusRep

instance (SetterFl p1 q1, SetterFl p2 q2, HasBinaryCoproducts k) => SetterFl (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 (Rep s ~> (PlusRep @ b)
d :.: (p1 a1 b1
l1 :**: p2 a2 b2
l2) :.: Rep (a1 ~> b1
f1 :**: a2 ~> b2
f2)) (Corep (a1 ~> b1
g1 :**: a2 ~> b2
g2) :.: (q1 a1 b1
r1 :**: q2 a2 b2
r2) :.: Corep (PlusRep @ b) ~> t
c) a ~> b
f =
    (PlusRep @ b) ~> t
(b1 || b2) ~> t
c ((b1 || b2) ~> t) -> (s ~> (b1 || b2)) -> s ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT 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).
SetterFl 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).
SetterFl p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
overP @p1 @q1 ((b1 ~> a) -> p1 a1 b1 -> p1 a1 a
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 b1 ~> a
a1 ~> b1
f1 p1 a1 b1
l1) ((b ~> a1) -> q1 a1 b1 -> q1 b b1
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 b ~> a1
a1 ~> b1
g1 q1 a1 b1
r1) a ~> b
f ((Fst @ b) ~> b1)
-> ((Snd @ b) ~> b2) -> ((Fst @ b) || (Snd @ b)) ~> (b1 || b2)
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).
SetterFl 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).
SetterFl p q =>
p s a -> q b t -> (a ~> b) -> s ~> t
overP @p2 @q2 ((b2 ~> a) -> p2 a2 b2 -> p2 a2 a
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 b2 ~> a
a2 ~> b2
f2 p2 a2 b2
l2) ((b ~> a2) -> q2 a2 b2 -> q2 b b2
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 b ~> a2
a2 ~> b2
g2 q2 a2 b2
r2) a ~> b
f) (((Fst @ b) || (Snd @ b)) ~> (b1 || b2))
-> (s ~> ((Fst @ b) || (Snd @ b))) -> s ~> (b1 || b2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (PlusRep @ b)
s ~> ((Fst @ b) || (Snd @ b))
d
instance
  (FoldFl p1 q1, FoldFl p2 q2, HasBinaryCoproducts k)
  => FoldFl (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 (Rep s ~> (PlusRep @ b)
d :.: (p1 a1 b1
l1 :**: p2 a2 b2
l2) :.: Rep (a1 ~> b1
f1 :**: a2 ~> b2
f2)) a ~> m
am =
    (forall {j} {k} (p :: k +-> k) (q :: j +-> j) (m :: k) (s :: k)
       (a :: k).
(FoldFl p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
forall (p :: k +-> k) (q :: k +-> k) (m :: k) (s :: k) (a :: k).
(FoldFl p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
foldMapP @p1 @q1 ((b1 ~> a) -> p1 a1 b1 -> p1 a1 a
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 b1 ~> a
a1 ~> b1
f1 p1 a1 b1
l1) a ~> m
am ((Fst @ b) ~> m)
-> ((Snd @ b) ~> m) -> ((Fst @ b) || (Snd @ b)) ~> 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).
(FoldFl p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
forall (p :: k +-> k) (q :: k +-> k) (m :: k) (s :: k) (a :: k).
(FoldFl p q, Monoid m) =>
p s a -> (a ~> m) -> s ~> m
foldMapP @p2 @q2 ((b2 ~> a) -> p2 a2 b2 -> p2 a2 a
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 b2 ~> a
a2 ~> b2
f2 p2 a2 b2
l2) a ~> m
am) (((Fst @ b) || (Snd @ b)) ~> m)
-> (s ~> ((Fst @ b) || (Snd @ b))) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (PlusRep @ b)
s ~> ((Fst @ b) || (Snd @ b))
d
instance (TravFl p1 q1, TravFl p2 q2, HasBinaryCoproducts k) => TravFl (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 (Rep s ~> (PlusRep @ b)
d :.: (p1 a1 b1
l1 :**: p2 a2 b2
l2) :.: Rep (a1 ~> b1
f1 :**: a2 ~> b2
f2)) (Corep (a1 ~> b1
g1 :**: a2 ~> b2
g2) :.: (q1 a1 b1
r1 :**: q2 a2 b2
r2) :.: Corep (PlusRep @ b) ~> t
c) r a b
r =
    (s ~> ((Fst @ b) || (Snd @ b)))
-> ((b1 || b2) ~> t)
-> r ((Fst @ b) || (Snd @ b)) (b1 || b2)
-> 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 ~> (PlusRep @ b)
s ~> ((Fst @ b) || (Snd @ b))
d (PlusRep @ b) ~> t
(b1 || b2) ~> t
c (forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(TravFl 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).
(TravFl p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP @p1 @q1 ((b1 ~> a) -> p1 a1 b1 -> p1 a1 a
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 b1 ~> a
a1 ~> b1
f1 p1 a1 b1
l1) ((b ~> a1) -> q1 a1 b1 -> q1 b b1
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 b ~> a1
a1 ~> b1
g1 q1 a1 b1
r1) r a b
r r a1 b1 -> r a2 b2 -> r (a1 || a2) (b1 || b2)
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).
(TravFl 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).
(TravFl p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP @p2 @q2 ((b2 ~> a) -> p2 a2 b2 -> p2 a2 a
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 b2 ~> a
a2 ~> b2
f2 p2 a2 b2
l2) ((b ~> a2) -> q2 a2 b2 -> q2 b b2
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 b ~> a2
a2 ~> b2
g2 q2 a2 b2
r2) r a b
r)
instance
  (MonTravFl p1 q1, MonTravFl p2 q2, HasBinaryCoproducts k)
  => MonTravFl (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 (Rep s ~> (PlusRep @ b)
d :.: (p1 a1 b1
l1 :**: p2 a2 b2
l2) :.: Rep (a1 ~> b1
f1 :**: a2 ~> b2
f2)) (Corep (a1 ~> b1
g1 :**: a2 ~> b2
g2) :.: (q1 a1 b1
r1 :**: q2 a2 b2
r2) :.: Corep (PlusRep @ b) ~> t
c) r a b
r =
    (s ~> ((Fst @ b) || (Snd @ b)))
-> ((b1 || b2) ~> t)
-> r ((Fst @ b) || (Snd @ b)) (b1 || b2)
-> 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 ~> (PlusRep @ b)
s ~> ((Fst @ b) || (Snd @ b))
d (PlusRep @ b) ~> t
(b1 || b2) ~> t
c (forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravFl 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).
(MonTravFl p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
monTravP @p1 @q1 ((b1 ~> a) -> p1 a1 b1 -> p1 a1 a
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 b1 ~> a
a1 ~> b1
f1 p1 a1 b1
l1) ((b ~> a1) -> q1 a1 b1 -> q1 b b1
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 b ~> a1
a1 ~> b1
g1 q1 a1 b1
r1) r a b
r r a1 b1 -> r a2 b2 -> r (a1 || a2) (b1 || b2)
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).
(MonTravFl 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).
(MonTravFl p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
monTravP @p2 @q2 ((b2 ~> a) -> p2 a2 b2 -> p2 a2 a
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 b2 ~> a
a2 ~> b2
f2 p2 a2 b2
l2) ((b ~> a2) -> q2 a2 b2 -> q2 b b2
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 b ~> a2
a2 ~> b2
g2 q2 a2 b2
r2) r a b
r)

-- | Witness pair with no foci at all: decompose to 'Unit' and rebuild.
--
-- 'UnitW' and 'CoUnitW' are the halves of 'Proarrow.Profunctor.Instance.Day.DayUnit', one per side,
-- with a phantom focus; with 'Beside'\/'CoBeside' they are the Day-monoidal structure on profunctors
-- split at the focus. The split is forced: a whole 'DayUnit' on the decomposition side would demand
-- @Unit ~> a@ for an arbitrary focus @a@.
--
-- Unlike 'Beside' this is not a composite: the nullary analogue would pass through the unit
-- category @()@, which can coincide with @k@ and so overlap the generic composition instances.
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 :: CAT 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 :: CAT 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) => SetterFl (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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> Unit
h
instance (Monoidal k) => FoldFl (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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> Unit
h
instance (Monoidal k) => TravFl (UnitW :: k +-> k) CoUnitW
instance (Monoidal k) => MonTravFl (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 :: CAT 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 :: CAT 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 :: CAT 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. These are 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 :: CAT 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 :: CAT 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) => SetterFl (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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> InitialObject
h
instance (HasInitialObject k) => FoldFl (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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> InitialObject
h
instance (HasInitialObject k) => TravFl (ZeroW :: k +-> k) CoZeroW
instance (HasInitialObject k) => MonTravFl (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 :: CAT 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 :: CAT 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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> InitialObject
h

-- * Van Laarhoven traversals

-- | The van Laarhoven form of a traversal with target @t@ and new focus @b@, as a functor of the
-- old focus @a@: run with any applicative handling of the foci.
type Baz :: Type -> Type -> Type -> Type
newtype Baz t b a = Baz {forall t b a.
Baz t b a
-> forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t
runBaz :: forall f. (P.Applicative f) => (a -> f b) -> f t}

instance P.Functor (Baz t b) where
  fmap :: forall a b. (a -> b) -> Baz t b a -> Baz t b b
fmap a -> b
f (Baz forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t
m) = (forall (f :: Type -> Type). Applicative f => (b -> f b) -> f t)
-> Baz t b b
forall t b a.
(forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t)
-> Baz t b a
Baz (\b -> f b
k -> (a -> f b) -> f t
forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t
m (b -> f b
k (b -> f b) -> (a -> b) -> a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
P.. a -> b
f))

instance P.Foldable (Baz t b) where
  foldMap :: forall m a. Monoid m => (a -> m) -> Baz t b a -> m
foldMap a -> m
f (Baz forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t
m) = Const m t -> m
forall {k} a (b :: k). Const a b -> a
getConst ((a -> Const m b) -> Const m t
forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t
m (m -> Const m b
forall {k} a (b :: k). a -> Const a b
Const (m -> Const m b) -> (a -> m) -> a -> Const m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
P.. a -> m
f))

-- | Handle the foci, keeping the rest of the traversal: run at @'Compose' f ('Bazaar' a' b)@.
instance P.Traversable (Baz t b) where
  traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Baz t b a -> f (Baz t b b)
traverse a -> f b
k (Baz forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t
m) = (Bazaar b b t -> Baz t b b) -> f (Bazaar b b t) -> f (Baz t b b)
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (\(Bazaar forall (f :: Type -> Type). Applicative f => (b -> f b) -> f t
m') -> (forall (f :: Type -> Type). Applicative f => (b -> f b) -> f t)
-> Baz t b b
forall t b a.
(forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t)
-> Baz t b a
Baz (b -> f b) -> f t
forall (f :: Type -> Type). Applicative f => (b -> f b) -> f t
m') (Compose f (Bazaar b b) t -> f (Bazaar b b t)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose ((a -> Compose f (Bazaar b b) b) -> Compose f (Bazaar b b) t
forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t
m (\a
a -> f (Bazaar b b b) -> Compose f (Bazaar b b) b
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((b -> Bazaar b b b) -> f b -> f (Bazaar b b b)
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (\b
a' -> (forall (f :: Type -> Type). Applicative f => (b -> f b) -> f b)
-> Bazaar b b b
forall a b t.
(forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t)
-> Bazaar a b t
Bazaar (\b -> f b
k' -> b -> f b
k' b
a')) (a -> f b
k a
a)))))

-- 'Baz' with its arguments in the order that makes it applicative in the result, for 'P.traverse'.
newtype Bazaar a b t = Bazaar (forall f. (P.Applicative f) => (a -> f b) -> f t)

instance P.Functor (Bazaar a b) where
  fmap :: forall a b. (a -> b) -> Bazaar a b a -> Bazaar a b b
fmap a -> b
f (Bazaar forall (f :: Type -> Type). Applicative f => (a -> f b) -> f a
m) = (forall (f :: Type -> Type). Applicative f => (a -> f b) -> f b)
-> Bazaar a b b
forall a b t.
(forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t)
-> Bazaar a b t
Bazaar (\a -> f b
k -> (a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap a -> b
f ((a -> f b) -> f a
forall (f :: Type -> Type). Applicative f => (a -> f b) -> f a
m a -> f b
k))

instance P.Applicative (Bazaar a b) where
  pure :: forall a. a -> Bazaar a b a
pure a
t = (forall (f :: Type -> Type). Applicative f => (a -> f b) -> f a)
-> Bazaar a b a
forall a b t.
(forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t)
-> Bazaar a b t
Bazaar (\a -> f b
_ -> a -> f a
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
P.pure a
t)
  Bazaar forall (f :: Type -> Type).
Applicative f =>
(a -> f b) -> f (a -> b)
mf <*> :: forall a b. Bazaar a b (a -> b) -> Bazaar a b a -> Bazaar a b b
<*> Bazaar forall (f :: Type -> Type). Applicative f => (a -> f b) -> f a
mx = (forall (f :: Type -> Type). Applicative f => (a -> f b) -> f b)
-> Bazaar a b b
forall a b t.
(forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t)
-> Bazaar a b t
Bazaar (\a -> f b
k -> (a -> f b) -> f (a -> b)
forall (f :: Type -> Type).
Applicative f =>
(a -> f b) -> f (a -> b)
mf a -> f b
k f (a -> b) -> f a -> f b
forall a b. f (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
P.<*> (a -> f b) -> f a
forall (f :: Type -> Type). Applicative f => (a -> f b) -> f a
mx a -> f b
k)

-- | Rebuild the target once every focus has its new type: run at 'Identity'.
sold :: Baz t b b -> t
sold :: forall t b. Baz t b b -> t
sold (Baz forall (f :: Type -> Type). Applicative f => (b -> f b) -> f t
m) = Identity t -> t
forall a. Identity a -> a
runIdentity ((b -> Identity b) -> Identity t
forall (f :: Type -> Type). Applicative f => (b -> f b) -> f t
m b -> Identity b
forall a. a -> Identity a
Identity)

-- | Build a 'Traversal' from a Prelude traversal such as 'P.traverse'. Its witness is
-- @'Star' ('Prelude' ('Baz' t b))@ with the function as the left leg, so this does no work;
-- eliminating the result distributes the carrier through 'traverse' at the witness.
fromTravVL :: forall s t a b. (forall f. (P.Applicative f) => (a -> f b) -> s -> f t) -> Traversal s t a b
fromTravVL :: forall s t a b.
(forall (f :: Type -> Type).
 Applicative f =>
 (a -> f b) -> s -> f t)
-> Traversal s t a b
fromTravVL forall (f :: Type -> Type). Applicative f => (a -> f b) -> s -> f t
f =
  forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR Type Type) (p :: Type +-> Type)
       (q :: Type +-> Type) s t a b.
(CategoryOf Type, CategoryOf Type, w p q, Profunctor p,
 Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @TravFl @(Star (Prelude (Baz t b))) @(RepCostar (Star (Prelude (Baz t b))))
    ((s ~> Prelude (Baz t b) a) -> Star (Prelude (Baz t b)) s a
forall {j} {k} (b :: j) (a :: k) (f :: j -> k).
Ob b =>
(a ~> f b) -> Star f a b
Star (\s
s -> Baz t b a -> Prelude (Baz t b) a
forall (f :: Type -> Type) a. f a -> Prelude f a
Prelude ((forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t)
-> Baz t b a
forall t b a.
(forall (f :: Type -> Type). Applicative f => (a -> f b) -> f t)
-> Baz t b a
Baz ((a -> f b) -> s -> f t
forall (f :: Type -> Type). Applicative f => (a -> f b) -> s -> f t
`f` s
s))))
    (((Star (Prelude (Baz t b)) % b) ~> t)
-> RepCostar (Star (Prelude (Baz t b))) b t
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (Baz t b b -> t
forall t b. Baz t b b -> t
sold (Baz t b b -> t)
-> (Prelude (Baz t b) b -> Baz t b b) -> Prelude (Baz t b) b -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Prelude (Baz t b) b -> Baz t b b
forall (f :: Type -> Type) a. Prelude f a -> f a
unPrelude))