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

-- | The __monoidal traversal__ optic and its free-profunctor apparatus. The mutually recursive
-- 'TravFl'\/'MonTravFl' flavor classes and their leaf instances live in
-- "Proarrow.Optic.Traversal". A 'MonoidalTraversal' distributes any
-- 'StrongDistributiveProfunctor' with no product-strength requirement; the profunctor-class
-- encoding 'PTraversal' converts to and from it via 'toPTraversal'\/'fromPTraversal', the latter
-- through the generic carrier @'ExOptic' 'MonTravFl'@, made an SDP here by generators (the Day
-- halves, the tensor-action witness @'Rep'@\/@'Corep'@ @('ActionAt' 'Tensor' _)@ and the coproduct prism).
module Proarrow.Optic.MonoidalTraversal where

import GHC.Generics qualified as G
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal, Tensor)
import Proarrow.Category.Monoidal.Action (ActionAt, CoprodAction, ProdAction)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Category.Monoidal.Distributive
  ( Distributive
  , StrongDistributiveProfunctor
  , Traversable
  , Traversing (..)
  )
import Proarrow.Category.Monoidal.Strength (Strong (..), strongId)
import Proarrow.Colimit.BinaryCoproduct
  ( COPROD (..)
  , Coprod (..)
  , Coproduct
  , HasBinaryCoproducts (..)
  , HasCoproducts
  , nil
  , (++)
  )
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), UN, type (+->), type (:&&:))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), HasProducts, PROD (..), Product)
import Proarrow.Object (pattern Objs)
import Proarrow.Optic
  ( ExOptic (..)
  , FLAVOR
  , Flavor
  , Optic
  , Optic_ (..)
  , Prostrong (..)
  , convert
  , withLegs
  )
import Proarrow.Optic.Traversal
  ( Beside
  , BesideSum
  , CoBeside
  , CoBesideSum
  , CoUnitW (..)
  , CoZeroW (..)
  , MonTravFl (..)
  , TravFl (..)
  , Traversal
  , UnitW (..)
  , ZeroW (..)
  )
import Proarrow.Profunctor.Corepresentable (Corep, Corepresentable (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Representable (Rep, RepCostar, Representable (..))
import Prelude (Either (..), const, either, uncurry, ($))

type MonoidalTraversal (s :: k) (t :: k) a b = Optic (Prostrong MonTravFl) s t a b
type MonoidalTraversal' s a = MonoidalTraversal s s a a

-- * The generic carrier is a strong distributive profunctor, by generators

-- Each piece of 'StrongDistributiveProfunctor' structure on @'ExOptic' w a b@ composes one more
-- generating witness pair onto the legs, so each instance holds for any closed flavor @w@ containing
-- that generator: 'UnitW'\/'Beside' for the tensor, 'ZeroW'\/'BesideSum' for the coproduct, the
-- tensor-action pair for tensor strength, and the prism and lens witnesses for the action
-- strengths. So 'PTraversal' and 'PTraversalFull' can be eliminated through 'ExOptic' by the
-- generic eliminators ('Proarrow.Optic.Setter.over', 'Proarrow.Optic.Fold.foldMapOf', ...), and
-- 'fromPTraversal' instantiates at this carrier.

exBeside
  :: forall {k} (w :: FLAVOR k k) (a :: k) b s1 t1 s2 t2
   . ( Monoidal k
     , forall p1 p2 q1 q2
        . (w p1 q1, w p2 q2, Profunctor p1, Profunctor p2, Profunctor q1, Profunctor q2)
       => w (Beside p1 p2) (CoBeside q1 q2)
     )
  => ExOptic w a b s1 t1 -> ExOptic w a b s2 t2 -> ExOptic w a b (s1 ** s2) (t1 ** t2)
exBeside :: forall {k} (w :: FLAVOR k k) (a :: k) (b :: k) (s1 :: k) (t1 :: k)
       (s2 :: k) (t2 :: k).
(Monoidal k,
 forall (p1 :: k +-> k) (p2 :: k +-> k) (q1 :: k +-> k)
        (q2 :: k +-> k).
 (w p1 q1, w p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
  Profunctor q2) =>
 w (Beside p1 p2) (CoBeside q1 q2)) =>
ExOptic w a b s1 t1
-> ExOptic w a b s2 t2 -> ExOptic w a b (s1 ** s2) (t1 ** t2)
exBeside (ExOptic @p1 @q1 l1 :: p s1 a
l1@p s1 a
Objs r1 :: q b t1
r1@q b t1
Objs) (ExOptic @p2 @q2 l2 :: p s2 a
l2@p s2 a
Objs r2 :: q b t2
r2@q b t2
Objs) =
  forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @s1 @s2 ((Ob (s1 ** s2) => ExOptic w a b (s1 ** s2) (t1 ** t2))
 -> ExOptic w a b (s1 ** s2) (t1 ** t2))
-> (Ob (s1 ** s2) => ExOptic w a b (s1 ** s2) (t1 ** t2))
-> ExOptic w a b (s1 ** s2) (t1 ** t2)
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @t1 @t2 ((Ob (t1 ** t2) => ExOptic w a b (s1 ** s2) (t1 ** t2))
 -> ExOptic w a b (s1 ** s2) (t1 ** t2))
-> (Ob (t1 ** t2) => ExOptic w a b (s1 ** s2) (t1 ** t2))
-> ExOptic w a b (s1 ** s2) (t1 ** t2)
forall a b. (a -> b) -> a -> b
$
      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 s a -> q b t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> ExOptic w a b s t
ExOptic @(Beside p1 p2) @(CoBeside q1 q2)
        (Rep MultRep (Rep MultRep % '(s1, s2)) '(s1, s2)
Rep MultRep (s1 ** s2) '(s1, s2)
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (a :: (k, k)). Ob a => Rep MultRep (Rep MultRep % a) a
repUniv Rep MultRep (s1 ** s2) '(s1, s2)
-> (:**:) p p '(s1, s2) '(a, a)
-> (:.:) (Rep MultRep) (p :**: p) (s1 ** s2) '(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
:.: (p s1 a
l1 p s1 a -> p s2 a -> (:**:) p p '(s1, s2) '(a, a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: p s2 a
l2) (:.:) (Rep MultRep) (p :**: p) (s1 ** s2) '(a, a)
-> Rep Diag '(a, a) a -> Beside p p (s1 ** s2) 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
:.: Rep Diag '(a, a) a
Rep Diag (Rep Diag % a) a
forall (a :: k). Ob a => Rep Diag (Rep Diag % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv)
        (Corep Diag b '(b, b)
Corep Diag b (Corep Diag %% b)
forall (a :: k). Ob a => Corep Diag a (Corep Diag %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv Corep Diag b '(b, b)
-> (:**:) q q '(b, b) '(t1, t2)
-> (:.:) (Corep Diag) (q :**: q) b '(t1, 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
:.: (q b t1
r1 q b t1 -> q b t2 -> (:**:) q q '(b, b) '(t1, t2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q b t2
r2) (:.:) (Corep Diag) (q :**: q) b '(t1, t2)
-> Corep MultRep '(t1, t2) (t1 ** t2) -> CoBeside q q b (t1 ** 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
:.: Corep MultRep '(t1, t2) (Corep MultRep %% '(t1, t2))
Corep MultRep '(t1, t2) (t1 ** t2)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (a :: (k, k)). Ob a => Corep MultRep a (Corep MultRep %% a)
corepUniv)

exBesideSum
  :: forall {k} (w :: FLAVOR k k) (a :: k) b s1 t1 s2 t2
   . ( HasBinaryCoproducts k
     , forall p1 p2 q1 q2
        . (w p1 q1, w p2 q2, Profunctor p1, Profunctor p2, Profunctor q1, Profunctor q2)
       => w (BesideSum p1 p2) (CoBesideSum q1 q2)
     )
  => ExOptic w a b s1 t1 -> ExOptic w a b s2 t2 -> ExOptic w a b (s1 || s2) (t1 || t2)
exBesideSum :: forall {k} (w :: FLAVOR k k) (a :: k) (b :: k) (s1 :: k) (t1 :: k)
       (s2 :: k) (t2 :: k).
(HasBinaryCoproducts k,
 forall (p1 :: k +-> k) (p2 :: k +-> k) (q1 :: k +-> k)
        (q2 :: k +-> k).
 (w p1 q1, w p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
  Profunctor q2) =>
 w (BesideSum p1 p2) (CoBesideSum q1 q2)) =>
ExOptic w a b s1 t1
-> ExOptic w a b s2 t2 -> ExOptic w a b (s1 || s2) (t1 || t2)
exBesideSum (ExOptic @p1 @q1 l1 :: p s1 a
l1@p s1 a
Objs r1 :: q b t1
r1@q b t1
Objs) (ExOptic @p2 @q2 l2 :: p s2 a
l2@p s2 a
Objs r2 :: q b t2
r2@q b t2
Objs) =
  forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @s1 @s2 ((Ob (s1 || s2) => ExOptic w a b (s1 || s2) (t1 || t2))
 -> ExOptic w a b (s1 || s2) (t1 || t2))
-> (Ob (s1 || s2) => ExOptic w a b (s1 || s2) (t1 || t2))
-> ExOptic w a b (s1 || s2) (t1 || t2)
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @t1 @t2 ((Ob (t1 || t2) => ExOptic w a b (s1 || s2) (t1 || t2))
 -> ExOptic w a b (s1 || s2) (t1 || t2))
-> (Ob (t1 || t2) => ExOptic w a b (s1 || s2) (t1 || t2))
-> ExOptic w a b (s1 || s2) (t1 || t2)
forall a b. (a -> b) -> a -> b
$
      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 s a -> q b t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> ExOptic w a b s t
ExOptic @(BesideSum p1 p2) @(CoBesideSum q1 q2)
        (Rep PlusRep (Rep PlusRep % '(s1, s2)) '(s1, s2)
Rep PlusRep (s1 || s2) '(s1, s2)
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (a :: (k, k)). Ob a => Rep PlusRep (Rep PlusRep % a) a
repUniv Rep PlusRep (s1 || s2) '(s1, s2)
-> (:**:) p p '(s1, s2) '(a, a)
-> (:.:) (Rep PlusRep) (p :**: p) (s1 || s2) '(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
:.: (p s1 a
l1 p s1 a -> p s2 a -> (:**:) p p '(s1, s2) '(a, a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: p s2 a
l2) (:.:) (Rep PlusRep) (p :**: p) (s1 || s2) '(a, a)
-> Rep Diag '(a, a) a -> BesideSum p p (s1 || s2) 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
:.: Rep Diag '(a, a) a
Rep Diag (Rep Diag % a) a
forall (a :: k). Ob a => Rep Diag (Rep Diag % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv)
        (Corep Diag b '(b, b)
Corep Diag b (Corep Diag %% b)
forall (a :: k). Ob a => Corep Diag a (Corep Diag %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv Corep Diag b '(b, b)
-> (:**:) q q '(b, b) '(t1, t2)
-> (:.:) (Corep Diag) (q :**: q) b '(t1, 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
:.: (q b t1
r1 q b t1 -> q b t2 -> (:**:) q q '(b, b) '(t1, t2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q b t2
r2) (:.:) (Corep Diag) (q :**: q) b '(t1, t2)
-> Corep PlusRep '(t1, t2) (t1 || t2)
-> CoBesideSum q q b (t1 || 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
:.: Corep PlusRep '(t1, t2) (Corep PlusRep %% '(t1, t2))
Corep PlusRep '(t1, t2) (t1 || t2)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (a :: (k, k)). Ob a => Corep PlusRep a (Corep PlusRep %% a)
corepUniv)

instance
  ( Monoidal k
  , Ob (a :: k)
  , Ob b
  , w UnitW CoUnitW
  , forall p1 p2 q1 q2
     . (w p1 q1, w p2 q2, Profunctor p1, Profunctor p2, Profunctor q1, Profunctor q2)
    => w (Beside p1 p2) (CoBeside q1 q2)
  )
  => MonoidalProfunctor (ExOptic w a b :: k +-> k)
  where
  one :: ExOptic w a b Unit Unit
one = UnitW Unit a -> CoUnitW b Unit -> ExOptic w a b Unit Unit
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 s a -> q b t -> ExOptic w a b s t
ExOptic ((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) ((Unit ~> Unit) -> CoUnitW b 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)
  ** :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
ExOptic w a b x1 x2
-> ExOptic w a b y1 y2 -> ExOptic w a b (x1 ** y1) (x2 ** y2)
(**) = ExOptic w a b x1 x2
-> ExOptic w a b y1 y2 -> ExOptic w a b (x1 ** y1) (x2 ** y2)
forall {k} (w :: FLAVOR k k) (a :: k) (b :: k) (s1 :: k) (t1 :: k)
       (s2 :: k) (t2 :: k).
(Monoidal k,
 forall (p1 :: k +-> k) (p2 :: k +-> k) (q1 :: k +-> k)
        (q2 :: k +-> k).
 (w p1 q1, w p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
  Profunctor q2) =>
 w (Beside p1 p2) (CoBeside q1 q2)) =>
ExOptic w a b s1 t1
-> ExOptic w a b s2 t2 -> ExOptic w a b (s1 ** s2) (t1 ** t2)
exBeside

instance
  ( HasCoproducts k
  , Ob (a :: k)
  , Ob b
  , w ZeroW CoZeroW
  , forall p1 p2 q1 q2
     . (w p1 q1, w p2 q2, Profunctor p1, Profunctor p2, Profunctor q1, Profunctor q2)
    => w (BesideSum p1 p2) (CoBesideSum q1 q2)
  )
  => MonoidalProfunctor (Coprod (ExOptic w a b :: k +-> k))
  where
  one :: Coprod (ExOptic w a b) Unit Unit
one = ExOptic w a b InitialObject InitialObject
-> Coprod (ExOptic w a b) (COPR InitialObject) (COPR InitialObject)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p (COPR a1) (COPR b1)
Coprod (ZeroW InitialObject a
-> CoZeroW b InitialObject
-> ExOptic w a b InitialObject InitialObject
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 s a -> q b t -> ExOptic w a b s t
ExOptic ((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) ((InitialObject ~> InitialObject) -> CoZeroW b 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))
  Coprod ExOptic w a b a1 b1
l ** :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod (ExOptic w a b) x1 x2
-> Coprod (ExOptic w a b) y1 y2
-> Coprod (ExOptic w a b) (x1 ** y1) (x2 ** y2)
** Coprod ExOptic w a b a1 b1
r = ExOptic w a b (a1 || a1) (b1 || b1)
-> Coprod (ExOptic w a b) (COPR (a1 || a1)) (COPR (b1 || b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p (COPR a1) (COPR b1)
Coprod (ExOptic w a b a1 b1
-> ExOptic w a b a1 b1 -> ExOptic w a b (a1 || a1) (b1 || b1)
forall {k} (w :: FLAVOR k k) (a :: k) (b :: k) (s1 :: k) (t1 :: k)
       (s2 :: k) (t2 :: k).
(HasBinaryCoproducts k,
 forall (p1 :: k +-> k) (p2 :: k +-> k) (q1 :: k +-> k)
        (q2 :: k +-> k).
 (w p1 q1, w p2 q2, Profunctor p1, Profunctor p2, Profunctor q1,
  Profunctor q2) =>
 w (BesideSum p1 p2) (CoBesideSum q1 q2)) =>
ExOptic w a b s1 t1
-> ExOptic w a b s2 t2 -> ExOptic w a b (s1 || s2) (t1 || t2)
exBesideSum ExOptic w a b a1 b1
l ExOptic w a b a1 b1
r)

instance
  ( Monoidal k
  , Ob (a :: k)
  , Ob b
  , Flavor w
  , forall (x :: k). (Ob x) => w (Rep (ActionAt Tensor x)) (Corep (ActionAt Tensor x))
  )
  => Strong Tensor (ExOptic w a b :: k +-> k)
  where
  act :: forall (a :: k) (x :: k) (y :: k).
Ob a =>
ExOptic w a b x y
-> ExOptic w a b (Act Tensor a x) (Act Tensor a y)
act @x @y @z (ExOptic @p @q l :: p x a
l@p x a
Objs r :: q b y
r@q b y
Objs) =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @x @y ((Ob (a ** x) => ExOptic w a b (Act Tensor a x) (Act Tensor a y))
 -> ExOptic w a b (Act Tensor a x) (Act Tensor a y))
-> (Ob (a ** x) => ExOptic w a b (Act Tensor a x) (Act Tensor a y))
-> ExOptic w a b (Act Tensor a x) (Act Tensor a y)
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @x @z ((Ob (a ** y) => ExOptic w a b (Act Tensor a x) (Act Tensor a y))
 -> ExOptic w a b (Act Tensor a x) (Act Tensor a y))
-> (Ob (a ** y) => ExOptic w a b (Act Tensor a x) (Act Tensor a y))
-> ExOptic w a b (Act Tensor a x) (Act Tensor a y)
forall a b. (a -> b) -> a -> b
$
        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 s a -> q b t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> ExOptic w a b s t
ExOptic @(Rep (ActionAt Tensor x) :.: p) @(q :.: Corep (ActionAt Tensor x)) (Rep (ActionAt Tensor a) (Rep (ActionAt Tensor a) % x) x
Rep (ActionAt Tensor a) (a ** x) x
forall (a :: k).
Ob a =>
Rep (ActionAt Tensor a) (Rep (ActionAt Tensor a) % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv Rep (ActionAt Tensor a) (a ** x) x
-> p x a -> (:.:) (Rep (ActionAt Tensor a)) p (a ** x) 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
:.: p x a
l) (q b y
r q b y
-> Corep (ActionAt Tensor a) y (a ** y)
-> (:.:) q (Corep (ActionAt Tensor a)) b (a ** y)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Corep (ActionAt Tensor a) y (Corep (ActionAt Tensor a) %% y)
Corep (ActionAt Tensor a) y (a ** y)
forall (a :: k).
Ob a =>
Corep (ActionAt Tensor a) a (Corep (ActionAt Tensor a) %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv)

instance
  ( HasCoproducts k
  , Ob (a :: k)
  , Ob b
  , Flavor w
  , forall (t :: k). (Ob t) => w (Rep (Coproduct t)) (Corep (Coproduct t))
  )
  => Strong CoprodAction (ExOptic w a b :: k +-> k)
  where
  act :: forall (a :: COPROD k) (x :: k) (y :: k).
Ob a =>
ExOptic w a b x y
-> ExOptic w a b (Act CoprodAction a x) (Act CoprodAction a y)
act @cx @y @z (ExOptic @p @q l :: p x a
l@p x a
Objs r :: q b y
r@q b y
Objs) =
    forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @(UN COPR cx) @y ((Ob (UN COPR a || x) =>
  ExOptic w a b (Act CoprodAction a x) (Act CoprodAction a y))
 -> ExOptic w a b (Act CoprodAction a x) (Act CoprodAction a y))
-> (Ob (UN COPR a || x) =>
    ExOptic w a b (Act CoprodAction a x) (Act CoprodAction a y))
-> ExOptic w a b (Act CoprodAction a x) (Act CoprodAction a y)
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @(UN COPR cx) @z ((Ob (UN COPR a || y) =>
  ExOptic w a b (Act CoprodAction a x) (Act CoprodAction a y))
 -> ExOptic w a b (Act CoprodAction a x) (Act CoprodAction a y))
-> (Ob (UN COPR a || y) =>
    ExOptic w a b (Act CoprodAction a x) (Act CoprodAction a y))
-> ExOptic w a b (Act CoprodAction a x) (Act CoprodAction a y)
forall a b. (a -> b) -> a -> b
$
        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 s a -> q b t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> ExOptic w a b s t
ExOptic @(Rep (Coproduct (UN COPR cx)) :.: p) @(q :.: Corep (Coproduct (UN COPR cx))) (Rep (Coproduct (UN COPR a)) (Rep (Coproduct (UN COPR a)) % x) x
Rep (Coproduct (UN COPR a)) (UN COPR a || x) x
forall (a :: k).
Ob a =>
Rep (Coproduct (UN COPR a)) (Rep (Coproduct (UN COPR a)) % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv Rep (Coproduct (UN COPR a)) (UN COPR a || x) x
-> p x a
-> (:.:) (Rep (Coproduct (UN COPR a))) p (UN COPR a || x) 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
:.: p x a
l) (q b y
r q b y
-> Corep (Coproduct (UN COPR a)) y (UN COPR a || y)
-> (:.:) q (Corep (Coproduct (UN COPR a))) b (UN COPR a || y)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Corep
  (Coproduct (UN COPR a)) y (Corep (Coproduct (UN COPR a)) %% y)
Corep (Coproduct (UN COPR a)) y (UN COPR a || y)
forall (a :: k).
Ob a =>
Corep
  (Coproduct (UN COPR a)) a (Corep (Coproduct (UN COPR a)) %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv)

instance
  (HasProducts k, Ob (a :: k), Ob b, Flavor w, forall (s :: k). (Ob s) => w (Rep (Product s)) (Corep (Product s)))
  => Strong ProdAction (ExOptic w a b :: k +-> k)
  where
  act :: forall (a :: PROD k) (x :: k) (y :: k).
Ob a =>
ExOptic w a b x y
-> ExOptic w a b (Act ProdAction a x) (Act ProdAction a y)
act @px @y @z (ExOptic @p @q l :: p x a
l@p x a
Objs r :: q b y
r@q b y
Objs) =
    forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @(UN PR px) @y ((Ob (UN PR a && x) =>
  ExOptic w a b (Act ProdAction a x) (Act ProdAction a y))
 -> ExOptic w a b (Act ProdAction a x) (Act ProdAction a y))
-> (Ob (UN PR a && x) =>
    ExOptic w a b (Act ProdAction a x) (Act ProdAction a y))
-> ExOptic w a b (Act ProdAction a x) (Act ProdAction a y)
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @(UN PR px) @z ((Ob (UN PR a && y) =>
  ExOptic w a b (Act ProdAction a x) (Act ProdAction a y))
 -> ExOptic w a b (Act ProdAction a x) (Act ProdAction a y))
-> (Ob (UN PR a && y) =>
    ExOptic w a b (Act ProdAction a x) (Act ProdAction a y))
-> ExOptic w a b (Act ProdAction a x) (Act ProdAction a y)
forall a b. (a -> b) -> a -> b
$
        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 s a -> q b t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> ExOptic w a b s t
ExOptic @(Rep (Product (UN PR px)) :.: p) @(q :.: Corep (Product (UN PR px))) (Rep (Product (UN PR a)) (Rep (Product (UN PR a)) % x) x
Rep (Product (UN PR a)) (UN PR a && x) x
forall (a :: k).
Ob a =>
Rep (Product (UN PR a)) (Rep (Product (UN PR a)) % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv Rep (Product (UN PR a)) (UN PR a && x) x
-> p x a -> (:.:) (Rep (Product (UN PR a))) p (UN PR a && x) 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
:.: p x a
l) (q b y
r q b y
-> Corep (Product (UN PR a)) y (UN PR a && y)
-> (:.:) q (Corep (Product (UN PR a))) b (UN PR a && y)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Corep (Product (UN PR a)) y (Corep (Product (UN PR a)) %% y)
Corep (Product (UN PR a)) y (UN PR a && y)
forall (a :: k).
Ob a =>
Corep (Product (UN PR a)) a (Corep (Product (UN PR a)) %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv)

-- | The generic carrier absorbs a traversable witness by composing the pair @t@\/@'RepCostar' t@
-- onto its legs with 'proact', like any other witness pair.
instance
  (CategoryOf k, Flavor w, forall t. (Traversable t, Representable t) => w t (RepCostar t))
  => Traversing (ExOptic w a b :: k +-> k)
  where
  traverseP :: forall (t :: k +-> k).
(Traversable t, Representable t) =>
(t :.: ExOptic w a b) :~> (ExOptic w a b :.: t)
traverseP @t (t a b
tx :.: ex :: ExOptic w a b b b
ex@(ExOptic p b a
_ q b b
Objs)) = forall {j} {k} (w :: FLAVOR j k) (p :: j +-> k) (f :: k +-> k)
       (g :: j +-> j).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
forall (w :: FLAVOR k k) (p :: k +-> k) (f :: k +-> k)
       (g :: k +-> k).
(Prostrong w p, w f g, Profunctor f, Profunctor g) =>
((f :.: p) :.: g) :~> p
proact @w (t a b
tx t a b -> ExOptic w a b b b -> (:.:) t (ExOptic w a b) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ExOptic w a b b b
ex (:.:) t (ExOptic w a b) a b
-> RepCostar t b (t % b)
-> (:.:) (t :.: ExOptic w a b) (RepCostar 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
:.: 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)) ExOptic w a b a (t % b)
-> t (t % b) b -> (:.:) (ExOptic w 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
:.: 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

-- | The other half of the equivalence between the encodings: instantiate the profunctor-class
-- traversal at @'ExOptic' 'MonTravFl' a b@, an SDP by the instances above. Its tensor strength
-- comes from the tensor-action witness @'Rep' ('ActionAt' 'Tensor' _)@, so this needs only
-- 'Proarrow.Category.Monoidal.CopyDiscard.CopyDiscard', already demanded by the coproduct prism,
-- and no 'Proarrow.Category.Monoidal.Cartesian.Cartesian'. So @Mat@ and @FinRel@ qualify, but
-- @LINEAR@, which cannot discard, does not. A 'Traversal' follows since 'MonTravFl' is a subflavor
-- of 'TravFl'.
fromPTraversal
  :: forall {k} (s :: k) (t :: k) a b
   . (Distributive k, CopyDiscard k, SymMonoidal k)
  => PTraversal s t a b -> MonoidalTraversal s t a b
fromPTraversal :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(Distributive k, CopyDiscard k, SymMonoidal k) =>
PTraversal s t a b -> MonoidalTraversal s t a b
fromPTraversal = Optic StrongDistributiveProfunctor s t a b
-> Optic (Prostrong MonTravFl) s t a b
forall {j} {k} (c :: (k -> j -> Type) -> Constraint)
       (w :: FLAVOR j k) (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b -> Optic (Prostrong w) s t a b
convert

-- | Like 'Proarrow.Optic.Traversal.traverseOf', but for a 'MonoidalTraversal': distributes any
-- 'StrongDistributiveProfunctor' with /no/ product-strength requirement on the carrier. Every non-lens traversal (prism,
-- 'Proarrow.Category.Monoidal.Distributive.Traversable' functor, ...) is a monoidal traversal, so this accepts carriers like @'Proarrow.Promonad.Writer.Writer' w@
-- that are tensor-strong but not product-strong.
--
-- Accepts any encoding (cf. 'Proarrow.Optic.Traversal.traverseOf'): a 'PTraversal' works directly,
-- as does a '(%)'-composite.
monTraverseOf
  :: forall {k} c (s :: k) (t :: k) a b p
   . (Distributive k, StrongDistributiveProfunctor p, (Ob a, Ob b) => c (ExOptic MonTravFl a b))
  => Optic c s t a b -> p a b -> p s t
monTraverseOf :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) (p :: k -> k -> Type).
(Distributive k, StrongDistributiveProfunctor p,
 (Ob a, Ob b) => c (ExOptic MonTravFl a b)) =>
Optic c s t a b -> p a b -> p s t
monTraverseOf 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 @MonTravFl 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).
(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 p s a
l q b t
r p a b
pab

-- | A traversal in the profunctor-class-flavored encoding (cf. 'Proarrow.Optic.PIso'), used by
-- the "GHC.Generics" combinators below. Equivalent to 'Traversal' via 'toPTraversal' and
-- 'fromPTraversal'.
type PTraversal s t a b = Optic StrongDistributiveProfunctor s t a b

type PTraversal' s a = PTraversal s s a a

-- | Half of the equivalence between the two traversal encodings: eliminate the existential
-- witnesses with 'travP' at the caller's profunctor.
toPTraversal
  :: forall {k} (s :: k) (t :: k) a b
   . (Distributive k)
  => MonoidalTraversal s t a b -> PTraversal s t a b
toPTraversal :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
Distributive k =>
MonoidalTraversal s t a b -> PTraversal s t a b
toPTraversal MonoidalTraversal s t a b
o = 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 @MonTravFl MonoidalTraversal s t a b
o \l :: p s a
l@p s a
Objs r :: q b t
r@q b t
Objs -> (forall (p :: k +-> k).
 (StrongDistributiveProfunctor p, Profunctor p) =>
 p a b -> p s t)
-> PTraversal s t a b
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic (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).
(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 p s a
l q b t
r)

-- | A full traversal in the profunctor-class encoding: distributes any profunctor carrying both
-- distributive strength and __product__ strength, the constraint 'travP' demands. This is
-- the 'Traversal' analog of 'PTraversal', which drops the product strength (all it needs for a
-- 'MonoidalTraversal'). Equivalent to 'Traversal' via 'toPTraversalFull' and 'traversal'.
type PTraversalFull s t a b = Optic (StrongDistributiveProfunctor :&&: Strong ProdAction) s t a b

-- | Build a 'Traversal' from its profunctor-class form, by instantiating the
-- rank-2 function at the generic carrier @'ExOptic' 'TravFl' a b@ (a 'StrongDistributiveProfunctor'
-- /and/ @'Strong' 'ProdAction'@, unlike @'ExOptic' 'MonTravFl' a b@, since 'TravFl' contains the
-- product-lens witness). The 'Traversal' analog of 'fromPTraversal'.
traversal
  :: forall {k} (s :: k) t a b
   . (Distributive k, CopyDiscard k, SymMonoidal k, HasProducts k, Ob a, Ob b, Ob s, Ob t)
  => (forall r. (StrongDistributiveProfunctor r, Strong ProdAction r) => r a b -> r s t) -> Traversal s t a b
traversal :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(Distributive k, CopyDiscard k, SymMonoidal k, HasProducts k, Ob a,
 Ob b, Ob s, Ob t) =>
(forall (r :: k +-> k).
 (StrongDistributiveProfunctor r, Strong ProdAction r) =>
 r a b -> r s t)
-> Traversal s t a b
traversal forall (r :: k +-> k).
(StrongDistributiveProfunctor r, Strong ProdAction r) =>
r a b -> r s t
f = Optic (StrongDistributiveProfunctor :&&: Strong ProdAction) s t a b
-> Optic (Prostrong TravFl) s t a b
forall {j} {k} (c :: (k -> j -> Type) -> Constraint)
       (w :: FLAVOR j k) (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b -> Optic (Prostrong w) s t a b
convert ((forall (p :: k +-> k).
 ((:&&:) StrongDistributiveProfunctor (Strong ProdAction) p,
  Profunctor p) =>
 p a b -> p s t)
-> Optic
     (StrongDistributiveProfunctor :&&: Strong ProdAction) s t a b
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic p a b -> p s t
forall (p :: k +-> k).
((:&&:) StrongDistributiveProfunctor (Strong ProdAction) p,
 Profunctor p) =>
p a b -> p s t
forall (r :: k +-> k).
(StrongDistributiveProfunctor r, Strong ProdAction r) =>
r a b -> r s t
f :: PTraversalFull s t a b)

-- | Eliminate a 'Traversal' to its profunctor-class form (the analog of 'toPTraversal'): run 'travP'
-- at the caller's profunctor.
toPTraversalFull
  :: forall {k} (s :: k) (t :: k) a b
   . (Distributive k)
  => Traversal s t a b -> PTraversalFull s t a b
toPTraversalFull :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
Distributive k =>
Traversal s t a b -> PTraversalFull s t a b
toPTraversalFull Traversal s t a b
o = 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 Traversal s t a b
o \l :: p s a
l@p s a
Objs r :: q b t
r@q b t
Objs -> (forall (p :: k +-> k).
 ((:&&:) StrongDistributiveProfunctor (Strong ProdAction) p,
  Profunctor p) =>
 p a b -> p s t)
-> PTraversalFull s t a b
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic (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)

v1Optic :: PTraversal (G.V1 a) (G.V1 a') a a'
v1Optic :: forall a a'. PTraversal (V1 a) (V1 a') a a'
v1Optic = (forall (p :: Type +-> Type).
 (StrongDistributiveProfunctor p, Profunctor p) =>
 p a a' -> p (V1 a) (V1 a'))
-> Optic_ (OPT a a') (OPT (V1 a) (V1 a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
_ -> (V1 a ~> Void)
-> (Void ~> V1 a') -> p Void Void -> p (V1 a) (V1 a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (\case {}) (\case {}) p Void Void
p InitialObject InitialObject
forall {j} {k} (p :: j +-> k).
MonoidalProfunctor (Coprod p) =>
p InitialObject InitialObject
nil

u1Optic :: PTraversal (G.U1 a) (G.U1 a') a a'
u1Optic :: forall a a'. PTraversal (U1 a) (U1 a') a a'
u1Optic = (forall (p :: Type +-> Type).
 (StrongDistributiveProfunctor p, Profunctor p) =>
 p a a' -> p (U1 a) (U1 a'))
-> Optic_ (OPT a a') (OPT (U1 a) (U1 a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
_ -> (U1 a ~> ()) -> (() ~> U1 a') -> p () () -> p (U1 a) (U1 a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (() -> U1 a -> ()
forall a b. a -> b -> a
const ()) (\() -> U1 a'
forall k (p :: k). U1 p
G.U1) p () ()
p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one

par1Optic :: PTraversal (G.Par1 a) (G.Par1 a') a a'
par1Optic :: forall a a'. PTraversal (Par1 a) (Par1 a') a a'
par1Optic = (forall (p :: Type +-> Type).
 (StrongDistributiveProfunctor p, Profunctor p) =>
 p a a' -> p (Par1 a) (Par1 a'))
-> Optic_ (OPT a a') (OPT (Par1 a) (Par1 a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic ((Par1 a ~> a) -> (a' ~> Par1 a') -> p a a' -> p (Par1 a) (Par1 a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap Par1 a ~> a
Par1 a -> a
forall p. Par1 p -> p
G.unPar1 a' ~> Par1 a'
a' -> Par1 a'
forall p. p -> Par1 p
G.Par1)

rec1Optic :: PTraversal (f a) (f a') a a' -> PTraversal (G.Rec1 f a) (G.Rec1 f a') a a'
rec1Optic :: forall (f :: Type -> Type) a a'.
PTraversal (f a) (f a') a a'
-> PTraversal (Rec1 f a) (Rec1 f a') a a'
rec1Optic (Optic forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
l) = (forall (p :: Type +-> Type).
 (StrongDistributiveProfunctor p, Profunctor p) =>
 p a a' -> p (Rec1 f a) (Rec1 f a'))
-> Optic_ (OPT a a') (OPT (Rec1 f a) (Rec1 f a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
p -> (Rec1 f a ~> s)
-> (t ~> Rec1 f a') -> p s t -> p (Rec1 f a) (Rec1 f a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap Rec1 f a ~> s
Rec1 f a -> f a
forall k (f :: k -> Type) (p :: k). Rec1 f p -> f p
G.unRec1 t ~> Rec1 f a'
f a' -> Rec1 f a'
forall k (f :: k -> Type) (p :: k). f p -> Rec1 f p
G.Rec1 (p a b -> p s t
forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
l p a a'
p a b
p)

m1Optic :: PTraversal (f a) (f a') a a' -> PTraversal (G.M1 i k f a) (G.M1 i k f a') a a'
m1Optic :: forall (f :: Type -> Type) a a' i (k :: Meta).
PTraversal (f a) (f a') a a'
-> PTraversal (M1 i k f a) (M1 i k f a') a a'
m1Optic (Optic forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
l) = (forall (p :: Type +-> Type).
 (StrongDistributiveProfunctor p, Profunctor p) =>
 p a a' -> p (M1 i k f a) (M1 i k f a'))
-> Optic_ (OPT a a') (OPT (M1 i k f a) (M1 i k f a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
p -> (M1 i k f a ~> s)
-> (t ~> M1 i k f a') -> p s t -> p (M1 i k f a) (M1 i k f a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap M1 i k f a ~> s
M1 i k f a -> f a
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
G.unM1 t ~> M1 i k f a'
f a' -> M1 i k f a'
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
G.M1 (p a b -> p s t
forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
l p a a'
p a b
p)

k1Optic :: forall i k a a'. PTraversal (G.K1 i k a) (G.K1 i k a') a a'
k1Optic :: forall i k a a'. PTraversal (K1 i k a) (K1 i k a') a a'
k1Optic = (forall (p :: Type +-> Type).
 (StrongDistributiveProfunctor p, Profunctor p) =>
 p a a' -> p (K1 i k a) (K1 i k a'))
-> Optic_ (OPT a a') (OPT (K1 i k a) (K1 i k a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
_ -> (K1 i k a ~> k)
-> (k ~> K1 i k a') -> p k k -> p (K1 i k a) (K1 i k a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap K1 i k a ~> k
K1 i k a -> k
forall k i c (p :: k). K1 i c p -> c
G.unK1 k ~> K1 i k a'
k -> K1 i k a'
forall k i c (p :: k). c -> K1 i c p
G.K1 p k k
forall {k} {p :: k +-> k} (a :: k).
(MonStrong p, MonoidalProfunctor p, Ob a) =>
p a a
strongId

plusOptic
  :: PTraversal (p a) (p a') a a'
  -> PTraversal (q a) (q a') a a'
  -> PTraversal ((p G.:+: q) a) ((p G.:+: q) a') a a'
plusOptic :: forall (p :: Type -> Type) a a' (q :: Type -> Type).
PTraversal (p a) (p a') a a'
-> PTraversal (q a) (q a') a a'
-> PTraversal ((:+:) p q a) ((:+:) p q a') a a'
plusOptic (Optic forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
l) (Optic forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
r) = (forall (p :: Type +-> Type).
 (StrongDistributiveProfunctor p, Profunctor p) =>
 p a a' -> p ((:+:) p q a) ((:+:) p q a'))
-> Optic_ (OPT a a') (OPT ((:+:) p q a) ((:+:) p q a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
p -> ((:+:) p q a ~> Either (p a) (q a))
-> (Either (p a') (q a') ~> (:+:) p q a')
-> p (Either (p a) (q a)) (Either (p a') (q a'))
-> p ((:+:) p q a) ((:+:) p q a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (\case G.L1 p a
f -> p a -> Either (p a) (q a)
forall a b. a -> Either a b
Left p a
f; G.R1 q a
f -> q a -> Either (p a) (q a)
forall a b. b -> Either a b
Right q a
f) ((p a' -> (:+:) p q a')
-> (q a' -> (:+:) p q a') -> Either (p a') (q a') -> (:+:) p q a'
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either p a' -> (:+:) p q a'
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
G.L1 q a' -> (:+:) p q a'
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
G.R1) (p a b -> p s t
forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
l p a a'
p a b
p p s t -> p s t -> p (s || s) (t || t)
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)
++ p a b -> p s t
forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
r p a a'
p a b
p)

multOptic
  :: PTraversal (p a) (p a') a a'
  -> PTraversal (q a) (q a') a a'
  -> PTraversal ((p G.:*: q) a) ((p G.:*: q) a') a a'
multOptic :: forall (p :: Type -> Type) a a' (q :: Type -> Type).
PTraversal (p a) (p a') a a'
-> PTraversal (q a) (q a') a a'
-> PTraversal ((:*:) p q a) ((:*:) p q a') a a'
multOptic (Optic forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
l) (Optic forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
r) = (forall (p :: Type +-> Type).
 (StrongDistributiveProfunctor p, Profunctor p) =>
 p a a' -> p ((:*:) p q a) ((:*:) p q a'))
-> Optic_ (OPT a a') (OPT ((:*:) p q a) ((:*:) p q a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
p -> ((:*:) p q a ~> (p a, q a))
-> ((p a', q a') ~> (:*:) p q a')
-> p (p a, q a) (p a', q a')
-> p ((:*:) p q a) ((:*:) p q a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (\(p a
f G.:*: q a
g) -> (p a
f, q a
g)) ((p a' -> q a' -> (:*:) p q a') -> (p a', q a') -> (:*:) p q a'
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry p a' -> q a' -> (:*:) p q a'
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(G.:*:)) (p a b -> p s t
forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
l p a a'
p a b
p p s t -> p s t -> p (s ** s) (t ** t)
forall x1 x2 y1 y2. p x1 x2 -> p y1 y2 -> p (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)
** p a b -> p s t
forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
r p a a'
p a b
p)

compOptic
  :: PTraversal (p (q a)) (p (q a')) (q a) (q a')
  -> PTraversal (q a) (q a') a a'
  -> PTraversal ((p G.:.: q) a) ((p G.:.: q) a') a a'
compOptic :: forall (p :: Type -> Type) (q :: Type -> Type) a a'.
PTraversal (p (q a)) (p (q a')) (q a) (q a')
-> PTraversal (q a) (q a') a a'
-> PTraversal ((:.:) p q a) ((:.:) p q a') a a'
compOptic (Optic forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
l) (Optic forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
r) = (forall (p :: Type +-> Type).
 (StrongDistributiveProfunctor p, Profunctor p) =>
 p a a' -> p ((:.:) p q a) ((:.:) p q a'))
-> Optic_ (OPT a a') (OPT ((:.:) p q a) ((:.:) p q a'))
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
(Ob a, Ob b, Ob s, Ob t) =>
(forall (p :: j +-> k). (c p, Profunctor p) => p a b -> p s t)
-> Optic_ (OPT a b) (OPT s t)
Optic \p a a'
p -> ((:.:) p q a ~> s)
-> (t ~> (:.:) p q a') -> p s t -> p ((:.:) p q a) ((:.:) p q a')
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (:.:) p q a ~> s
(:.:) p q a -> p (q a)
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
G.unComp1 t ~> (:.:) p q a'
p (q a') -> (:.:) p q a'
forall k2 k1 (f :: k2 -> Type) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
G.Comp1 (p a b -> p s t
forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
l (p a b -> p s t
forall (p :: Type +-> Type).
(StrongDistributiveProfunctor p, Profunctor p) =>
p a b -> p s t
r p a a'
p a b
p))