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

-- | The __monoidal traversal__ optic and its free-profunctor apparatus, split out of
-- "Proarrow.Optic.Traversal" (which keeps the mutually-recursive 'TravRes'\/'MonTravRes' flavor
-- classes and their leaf instances). 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 free 'MonTravRes'-strong profunctor @'ExOptic' 'MonTravRes'@ (an SDP, via the
-- tensor-strength witness 'TensorW').
module Proarrow.Optic.MonoidalTraversal where

import GHC.Generics qualified as G
import Proarrow.Adjunction (Proadjunction (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal, Tensor)
import Proarrow.Category.Monoidal.Action (CoprodAction, ProdAction)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Category.Monoidal.Distributive (Distributive, StrongDistributiveProfunctor)
import Proarrow.Category.Monoidal.Strength (Strong (..), strongId)
import Proarrow.Colimit.BinaryCoproduct
  ( COPROD (..)
  , Coprod (..)
  , Coproduct
  , HasBinaryCoproducts (..)
  , HasCoproducts
  , nil
  , (++)
  )
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), UN, obj, (\\), type (+->))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), HasProducts, PROD (..), Product)
import Proarrow.Object (pattern Objs)
import Proarrow.Optic
  ( CompactFlavor (..)
  , ExOptic (..)
  , IsOptic (..)
  , Optic
  , Optic_ (..)
  , Prostrong (..)
  , SubFlavor (..)
  , convert
  , ex2prof
  , withLegs
  , type (:&&:)
  )
import Proarrow.Optic.Fold (FoldRes (..))
import Proarrow.Optic.Setter (SetterRes (..))
import Proarrow.Optic.Traversal
  ( Beside (..)
  , BesideSum (..)
  , CoBeside (..)
  , CoBesideSum (..)
  , CoUnitW (..)
  , CoZeroW (..)
  , MonTravRes (..)
  , TravRes (..)
  , Traversal
  , UnitW (..)
  , ZeroW (..)
  )
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Representable (Rep (..))
import Prelude (Either (..), const, either, uncurry, ($))

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

-- | Witness pair for __tensor strength__: the focus @x@ sits inside @a '**' x@ with the residual
-- @a@ carried on the left. This is the tensor-action dual of the coproduct-action prism witness
-- @'Rep' ('Coproduct' t)@\/@'Corep' ('Coproduct' t)@ (whose 'monTravP' calls @'act' \@'CoprodAction'@):
-- here 'monTravP' calls @'act' \@'Tensor'@ -- exactly the strength any 'StrongDistributiveProfunctor'
-- already carries. Unlike the product-lens @'Rep' ('Product' a)@ that used to witness @'Strong'
-- 'Tensor'@ for the free traversal, this needs no @'Strong' 'ProdAction'@ and no @tensor = product@
-- ('Proarrow.Limit.BinaryProduct.Cartesian'): it is a genuine 'MonTravRes', so the free
-- monoidal-traversal profunctor @'ExOptic' 'MonTravRes'@ is 'Proarrow.Category.Monoidal.Strength.MonStrong'.
type TensorW :: forall {k}. k -> k +-> k
data TensorW a s x where
  TensorW :: (Ob a, Ob x) => (s ~> (a ** x)) -> TensorW a s x

-- | The covariant half of the 'TensorW' witness pair: rebuilds the target around the carried
-- residual, @(a '**' x) '~>' t@.
type CoTensorW :: forall {k}. k -> k +-> k
data CoTensorW a x t where
  CoTensorW :: (Ob a, Ob x) => ((a ** x) ~> t) -> CoTensorW a x t

instance (Monoidal k, Ob (a :: k)) => Profunctor (TensorW a :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> TensorW a a b -> TensorW a c d
dimap c ~> a
l b ~> d
r (TensorW a ~> (a ** b)
h) = (c ~> (a ** d)) -> TensorW a c d
forall {k} (a :: k) (x :: k) (s :: k).
(Ob a, Ob x) =>
(s ~> (a ** x)) -> TensorW a s x
TensorW ((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (b ~> d) -> (a ** b) ~> (a ** d)
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)
** b ~> d
r) ((a ** b) ~> (a ** d)) -> (c ~> (a ** b)) -> c ~> (a ** d)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (a ** b)
h (a ~> (a ** b)) -> (c ~> a) -> c ~> (a ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l) ((Ob b, Ob d) => TensorW a c d) -> (b ~> d) -> TensorW a 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) -> TensorW a a b -> r
\\ TensorW a ~> (a ** b)
h = r
(Ob a, Ob b) => r
(Ob a, Ob (a ** b)) => r
r ((Ob a, Ob (a ** b)) => r) -> (a ~> (a ** 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
\\ a ~> (a ** b)
h
instance (Monoidal k, Ob (a :: k)) => Profunctor (CoTensorW a :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> CoTensorW a a b -> CoTensorW a c d
dimap c ~> a
l b ~> d
r (CoTensorW (a ** a) ~> b
i) = ((a ** c) ~> d) -> CoTensorW a c d
forall {k} (a :: k) (x :: k) (t :: k).
(Ob a, Ob x) =>
((a ** x) ~> t) -> CoTensorW a x t
CoTensorW (b ~> d
r (b ~> d) -> ((a ** c) ~> b) -> (a ** c) ~> d
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ** a) ~> b
i ((a ** a) ~> b) -> ((a ** c) ~> (a ** a)) -> (a ** c) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (c ~> a) -> (a ** c) ~> (a ** a)
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)
** c ~> a
l)) ((Ob c, Ob a) => CoTensorW a c d) -> (c ~> a) -> CoTensorW a 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) -> CoTensorW a a b -> r
\\ CoTensorW (a ** a) ~> b
i = r
(Ob a, Ob b) => r
(Ob (a ** a), Ob b) => r
r ((Ob (a ** a), Ob b) => r) -> ((a ** a) ~> 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
\\ (a ** a) ~> b
i

instance (Monoidal k, Ob (a :: k)) => Proadjunction (TensorW a :: k +-> k) (CoTensorW a) where
  unit :: forall (a :: k). Ob a => (:.:) (CoTensorW a) (TensorW a) a a
unit @c = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @c (((a ** a) ~> (a ** a)) -> CoTensorW a a (a ** a)
forall {k} (a :: k) (x :: k) (t :: k).
(Ob a, Ob x) =>
((a ** x) ~> t) -> CoTensorW a x t
CoTensorW (a ** a) ~> (a ** a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id CoTensorW a a (a ** a)
-> TensorW a (a ** a) a -> (:.:) (CoTensorW a) (TensorW a) 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
:.: ((a ** a) ~> (a ** a)) -> TensorW a (a ** a) a
forall {k} (a :: k) (x :: k) (s :: k).
(Ob a, Ob x) =>
(s ~> (a ** x)) -> TensorW a s x
TensorW (a ** a) ~> (a ** a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  counit :: (TensorW a :.: CoTensorW a) :~> (~>)
counit (TensorW a ~> (a ** b)
h :.: CoTensorW (a ** b) ~> b
i) = (a ** b) ~> b
i ((a ** b) ~> b) -> (a ~> (a ** b)) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (a ** b)
h
instance (Monoidal k, Ob (a :: k)) => SetterRes (TensorW a :: k +-> k) (CoTensorW a) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
TensorW a s a -> CoTensorW a b t -> (a ~> b) -> s ~> t
overP (TensorW s ~> (a ** a)
h) (CoTensorW (a ** b) ~> t
i) a ~> b
f = (a ** b) ~> t
i ((a ** b) ~> t) -> (s ~> (a ** b)) -> s ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (a ~> b) -> (a ** a) ~> (a ** b)
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 ~> b
f) ((a ** a) ~> (a ** b)) -> (s ~> (a ** a)) -> s ~> (a ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (a ** a)
h
instance (CopyDiscard k, Ob (a :: k)) => FoldRes (TensorW a :: k +-> k) (CoTensorW a) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
TensorW a s a -> (a ~> m) -> s ~> m
foldMapP (TensorW s ~> (a ** 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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard @k @a (a ~> Unit) -> (a ~> m) -> (a ** 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) ((a ** a) ~> (Unit ** m)) -> (s ~> (a ** a)) -> s ~> (Unit ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (a ** a)
h
instance (CopyDiscard k, Ob (a :: k)) => TravRes (TensorW a :: k +-> k) (CoTensorW a)
instance (CopyDiscard k, Ob (a :: k)) => MonTravRes (TensorW a :: k +-> k) (CoTensorW a) where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
TensorW a s a -> CoTensorW a b t -> r a b -> r s t
monTravP (TensorW s ~> (a ** a)
h) (CoTensorW (a ** b) ~> t
i) r a b
r = (s ~> (a ** a)) -> ((a ** b) ~> t) -> r (a ** a) (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 ** a)
h (a ** 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 @_ @a r a b
r)

besideTensor
  :: forall {k} (a :: k) b s1 t1 s2 t2
   . (Monoidal k, Ob a, Ob b)
  => ExOptic MonTravRes a b s1 t1 -> ExOptic MonTravRes a b s2 t2 -> ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2)
besideTensor :: forall {k} (a :: k) (b :: k) (s1 :: k) (t1 :: k) (s2 :: k)
       (t2 :: k).
(Monoidal k, Ob a, Ob b) =>
ExOptic MonTravRes a b s1 t1
-> ExOptic MonTravRes a b s2 t2
-> ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2)
besideTensor ExOptic MonTravRes a b s1 t1
l ExOptic MonTravRes a b s2 t2
r =
  ExOptic MonTravRes a b s1 t1
-> (forall (p :: k +-> k) (q :: k +-> k).
    (MonTravRes p q, Profunctor p, Profunctor q) =>
    p s1 a -> q b t1 -> ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2))
-> ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2)
forall (a :: k) (b :: k) (s :: k) (t :: k) r.
(CategoryOf k, CategoryOf k) =>
ExOptic MonTravRes a b s t
-> (forall (p :: k +-> k) (q :: k +-> k).
    (MonTravRes p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall j k (w :: FLAVOR j k) (a :: k) (b :: j) (s :: k) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
ExOptic w a b s t
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
compress ExOptic MonTravRes a b s1 t1
l \p1 :: p s1 a
p1@p s1 a
Objs q1 :: q b t1
q1@q b t1
Objs ->
    ExOptic MonTravRes a b s2 t2
-> (forall (p :: k +-> k) (q :: k +-> k).
    (MonTravRes p q, Profunctor p, Profunctor q) =>
    p s2 a -> q b t2 -> ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2))
-> ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2)
forall (a :: k) (b :: k) (s :: k) (t :: k) r.
(CategoryOf k, CategoryOf k) =>
ExOptic MonTravRes a b s t
-> (forall (p :: k +-> k) (q :: k +-> k).
    (MonTravRes p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall j k (w :: FLAVOR j k) (a :: k) (b :: j) (s :: k) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
ExOptic w a b s t
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
compress ExOptic MonTravRes a b s2 t2
r \p2 :: p s2 a
p2@p s2 a
Objs q2 :: q b t2
q2@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 MonTravRes a b (s1 ** s2) (t1 ** t2))
 -> ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2))
-> (Ob (s1 ** s2) => ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2))
-> ExOptic MonTravRes 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 MonTravRes a b (s1 ** s2) (t1 ** t2))
 -> ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2))
-> (Ob (t1 ** t2) => ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2))
-> ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2)
forall a b. (a -> b) -> a -> b
$
          (:.:)
  (Beside p p :.: ExOptic MonTravRes a b)
  (CoBeside q q)
  (s1 ** s2)
  (t1 ** t2)
-> ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2)
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong (((s1 ** s2) ~> (s1 ** s2))
-> p s1 a -> p s2 a -> Beside p p (s1 ** s2) a
forall {k} (s :: k) (s1 :: k) (s2 :: k) (p1 :: k +-> k) (x :: k)
       (p2 :: k +-> k).
(s ~> (s1 ** s2)) -> p1 s1 x -> p2 s2 x -> Beside p1 p2 s x
Beside (s1 ** s2) ~> (s1 ** s2)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id p s1 a
p1 p s2 a
p2 Beside p p (s1 ** s2) a
-> ExOptic MonTravRes a b a b
-> (:.:) (Beside p p) (ExOptic MonTravRes a b) (s1 ** s2) b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic MonTravRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) (Beside p p) (ExOptic MonTravRes a b) (s1 ** s2) b
-> CoBeside q q b (t1 ** t2)
-> (:.:)
     (Beside p p :.: ExOptic MonTravRes a b)
     (CoBeside q q)
     (s1 ** s2)
     (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
-> q b t2
-> ((t1 ** t2) ~> (t1 ** t2))
-> CoBeside q q b (t1 ** t2)
forall {k} (q1 :: k +-> k) (x :: k) (t1 :: k) (q2 :: k +-> k)
       (t2 :: k) (t :: k).
q1 x t1 -> q2 x t2 -> ((t1 ** t2) ~> t) -> CoBeside q1 q2 x t
CoBeside q b t1
q1 q b t2
q2 (t1 ** t2) ~> (t1 ** t2)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

besideSum
  :: forall {k} (a :: k) b s1 t1 s2 t2
   . (HasBinaryCoproducts k, Ob a, Ob b)
  => ExOptic MonTravRes a b s1 t1 -> ExOptic MonTravRes a b s2 t2 -> ExOptic MonTravRes a b (s1 || s2) (t1 || t2)
besideSum :: forall {k} (a :: k) (b :: k) (s1 :: k) (t1 :: k) (s2 :: k)
       (t2 :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
ExOptic MonTravRes a b s1 t1
-> ExOptic MonTravRes a b s2 t2
-> ExOptic MonTravRes a b (s1 || s2) (t1 || t2)
besideSum ExOptic MonTravRes a b s1 t1
l ExOptic MonTravRes a b s2 t2
r =
  ExOptic MonTravRes a b s1 t1
-> (forall (p :: k +-> k) (q :: k +-> k).
    (MonTravRes p q, Profunctor p, Profunctor q) =>
    p s1 a -> q b t1 -> ExOptic MonTravRes a b (s1 || s2) (t1 || t2))
-> ExOptic MonTravRes a b (s1 || s2) (t1 || t2)
forall (a :: k) (b :: k) (s :: k) (t :: k) r.
(CategoryOf k, CategoryOf k) =>
ExOptic MonTravRes a b s t
-> (forall (p :: k +-> k) (q :: k +-> k).
    (MonTravRes p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall j k (w :: FLAVOR j k) (a :: k) (b :: j) (s :: k) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
ExOptic w a b s t
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
compress ExOptic MonTravRes a b s1 t1
l \p1 :: p s1 a
p1@p s1 a
Objs q1 :: q b t1
q1@q b t1
Objs ->
    ExOptic MonTravRes a b s2 t2
-> (forall (p :: k +-> k) (q :: k +-> k).
    (MonTravRes p q, Profunctor p, Profunctor q) =>
    p s2 a -> q b t2 -> ExOptic MonTravRes a b (s1 || s2) (t1 || t2))
-> ExOptic MonTravRes a b (s1 || s2) (t1 || t2)
forall (a :: k) (b :: k) (s :: k) (t :: k) r.
(CategoryOf k, CategoryOf k) =>
ExOptic MonTravRes a b s t
-> (forall (p :: k +-> k) (q :: k +-> k).
    (MonTravRes p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall j k (w :: FLAVOR j k) (a :: k) (b :: j) (s :: k) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
ExOptic w a b s t
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
compress ExOptic MonTravRes a b s2 t2
r \p2 :: p s2 a
p2@p s2 a
Objs q2 :: q b t2
q2@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 MonTravRes a b (s1 || s2) (t1 || t2))
 -> ExOptic MonTravRes a b (s1 || s2) (t1 || t2))
-> (Ob (s1 || s2) => ExOptic MonTravRes a b (s1 || s2) (t1 || t2))
-> ExOptic MonTravRes 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 MonTravRes a b (s1 || s2) (t1 || t2))
 -> ExOptic MonTravRes a b (s1 || s2) (t1 || t2))
-> (Ob (t1 || t2) => ExOptic MonTravRes a b (s1 || s2) (t1 || t2))
-> ExOptic MonTravRes a b (s1 || s2) (t1 || t2)
forall a b. (a -> b) -> a -> b
$
          (:.:)
  (BesideSum p p :.: ExOptic MonTravRes a b)
  (CoBesideSum q q)
  (s1 || s2)
  (t1 || t2)
-> ExOptic MonTravRes a b (s1 || s2) (t1 || t2)
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong (((s1 || s2) ~> (s1 || s2))
-> p s1 a -> p s2 a -> BesideSum p p (s1 || s2) a
forall {k} (s :: k) (s1 :: k) (s2 :: k) (p1 :: k +-> k) (x :: k)
       (p2 :: k +-> k).
(s ~> (s1 || s2)) -> p1 s1 x -> p2 s2 x -> BesideSum p1 p2 s x
BesideSum (s1 || s2) ~> (s1 || s2)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id p s1 a
p1 p s2 a
p2 BesideSum p p (s1 || s2) a
-> ExOptic MonTravRes a b a b
-> (:.:) (BesideSum p p) (ExOptic MonTravRes a b) (s1 || s2) b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic MonTravRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) (BesideSum p p) (ExOptic MonTravRes a b) (s1 || s2) b
-> CoBesideSum q q b (t1 || t2)
-> (:.:)
     (BesideSum p p :.: ExOptic MonTravRes a b)
     (CoBesideSum q q)
     (s1 || s2)
     (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
-> q b t2
-> ((t1 || t2) ~> (t1 || t2))
-> CoBesideSum q q b (t1 || t2)
forall {k} (q1 :: k +-> k) (x :: k) (t1 :: k) (q2 :: k +-> k)
       (t2 :: k) (t :: k).
q1 x t1 -> q2 x t2 -> ((t1 || t2) ~> t) -> CoBesideSum q1 q2 x t
CoBesideSum q b t1
q1 q b t2
q2 (t1 || t2) ~> (t1 || t2)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

instance (Monoidal k, Ob (a :: k), Ob b) => MonoidalProfunctor (ExOptic MonTravRes a b :: k +-> k) where
  one :: ExOptic MonTravRes a b Unit Unit
one = (:.:) (UnitW :.: ExOptic MonTravRes a b) CoUnitW Unit Unit
-> ExOptic MonTravRes 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 :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong ((Unit ~> Unit) -> UnitW Unit a
forall {k} (x :: k) (s :: k). Ob x => (s ~> Unit) -> UnitW s x
UnitW Unit ~> Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id UnitW Unit a
-> ExOptic MonTravRes a b a b
-> (:.:) UnitW (ExOptic MonTravRes a b) Unit b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic MonTravRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) UnitW (ExOptic MonTravRes a b) Unit b
-> CoUnitW b Unit
-> (:.:) (UnitW :.: ExOptic MonTravRes a b) CoUnitW Unit Unit
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) -> 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  ExOptic MonTravRes a b x1 x2
l ** :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
ExOptic MonTravRes a b x1 x2
-> ExOptic MonTravRes a b y1 y2
-> ExOptic MonTravRes a b (x1 ** y1) (x2 ** y2)
** ExOptic MonTravRes a b y1 y2
r = ExOptic MonTravRes a b x1 x2
-> ExOptic MonTravRes a b y1 y2
-> ExOptic MonTravRes a b (x1 ** y1) (x2 ** y2)
forall {k} (a :: k) (b :: k) (s1 :: k) (t1 :: k) (s2 :: k)
       (t2 :: k).
(Monoidal k, Ob a, Ob b) =>
ExOptic MonTravRes a b s1 t1
-> ExOptic MonTravRes a b s2 t2
-> ExOptic MonTravRes a b (s1 ** s2) (t1 ** t2)
besideTensor ExOptic MonTravRes a b x1 x2
l ExOptic MonTravRes a b y1 y2
r

instance (HasCoproducts k, Ob (a :: k), Ob b) => MonoidalProfunctor (Coprod (ExOptic MonTravRes a b :: k +-> k)) where
  one :: Coprod (ExOptic MonTravRes a b) Unit Unit
one = ExOptic MonTravRes a b InitialObject InitialObject
-> Coprod
     (ExOptic MonTravRes 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 :.: ExOptic MonTravRes a b)
  CoZeroW
  InitialObject
  InitialObject
-> ExOptic MonTravRes 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 :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong ((InitialObject ~> InitialObject) -> ZeroW InitialObject a
forall {k} (x :: k) (s :: k).
Ob x =>
(s ~> InitialObject) -> ZeroW s x
ZeroW InitialObject ~> InitialObject
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id ZeroW InitialObject a
-> ExOptic MonTravRes a b a b
-> (:.:) ZeroW (ExOptic MonTravRes a b) InitialObject b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic MonTravRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) ZeroW (ExOptic MonTravRes a b) InitialObject b
-> CoZeroW b InitialObject
-> (:.:)
     (ZeroW :.: ExOptic MonTravRes a b)
     CoZeroW
     InitialObject
     InitialObject
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) -> 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id))
  Coprod ExOptic MonTravRes a b a1 b1
l ** :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod (ExOptic MonTravRes a b) x1 x2
-> Coprod (ExOptic MonTravRes a b) y1 y2
-> Coprod (ExOptic MonTravRes a b) (x1 ** y1) (x2 ** y2)
** Coprod ExOptic MonTravRes a b a1 b1
r = ExOptic MonTravRes a b (a1 || a1) (b1 || b1)
-> Coprod
     (ExOptic MonTravRes 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 MonTravRes a b a1 b1
-> ExOptic MonTravRes a b a1 b1
-> ExOptic MonTravRes a b (a1 || a1) (b1 || b1)
forall {k} (a :: k) (b :: k) (s1 :: k) (t1 :: k) (s2 :: k)
       (t2 :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
ExOptic MonTravRes a b s1 t1
-> ExOptic MonTravRes a b s2 t2
-> ExOptic MonTravRes a b (s1 || s2) (t1 || t2)
besideSum ExOptic MonTravRes a b a1 b1
l ExOptic MonTravRes a b a1 b1
r)

instance (CopyDiscard k, Ob (a :: k), Ob b) => Strong Tensor (ExOptic MonTravRes a b :: k +-> k) where
  act :: forall (a :: k) (x :: k) (y :: k).
Ob a =>
ExOptic MonTravRes a b x y
-> ExOptic MonTravRes a b (Act Tensor a x) (Act Tensor a y)
act @x @y @z e :: ExOptic MonTravRes a b x y
e@ExOptic MonTravRes a b x 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 MonTravRes a b (Act Tensor a x) (Act Tensor a y))
 -> ExOptic MonTravRes a b (Act Tensor a x) (Act Tensor a y))
-> (Ob (a ** x) =>
    ExOptic MonTravRes a b (Act Tensor a x) (Act Tensor a y))
-> ExOptic MonTravRes 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 MonTravRes a b (Act Tensor a x) (Act Tensor a y))
 -> ExOptic MonTravRes a b (Act Tensor a x) (Act Tensor a y))
-> (Ob (a ** y) =>
    ExOptic MonTravRes a b (Act Tensor a x) (Act Tensor a y))
-> ExOptic MonTravRes 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 :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(MonTravRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic MonTravRes a b) q s t
-> ExOptic MonTravRes a b s t
ExProstrong @(TensorW x) @(CoTensorW x) (((a ** x) ~> (a ** x)) -> TensorW a (a ** x) x
forall {k} (a :: k) (x :: k) (s :: k).
(Ob a, Ob x) =>
(s ~> (a ** x)) -> TensorW a s x
TensorW (a ** x) ~> (a ** x)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id TensorW a (a ** x) x
-> ExOptic MonTravRes a b x y
-> (:.:) (TensorW a) (ExOptic MonTravRes a b) (a ** x) y
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ExOptic MonTravRes a b x y
e (:.:) (TensorW a) (ExOptic MonTravRes a b) (a ** x) y
-> CoTensorW a y (a ** y)
-> (:.:)
     (TensorW a :.: ExOptic MonTravRes a b)
     (CoTensorW a)
     (a ** x)
     (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
:.: ((a ** y) ~> (a ** y)) -> CoTensorW a y (a ** y)
forall {k} (a :: k) (x :: k) (t :: k).
(Ob a, Ob x) =>
((a ** x) ~> t) -> CoTensorW a x t
CoTensorW (a ** y) ~> (a ** y)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

instance (HasCoproducts k, CopyDiscard k, Ob (a :: k), Ob b) => Strong CoprodAction (ExOptic MonTravRes a b :: k +-> k) where
  act :: forall (a :: COPROD k) (x :: k) (y :: k).
Ob a =>
ExOptic MonTravRes a b x y
-> ExOptic
     MonTravRes a b (Act CoprodAction a x) (Act CoprodAction a y)
act @cx @y @z e :: ExOptic MonTravRes a b x y
e@ExOptic MonTravRes a b x 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
    MonTravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
 -> ExOptic
      MonTravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
-> (Ob (UN 'COPR a || x) =>
    ExOptic
      MonTravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
-> ExOptic
     MonTravRes 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
    MonTravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
 -> ExOptic
      MonTravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
-> (Ob (UN 'COPR a || y) =>
    ExOptic
      MonTravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
-> ExOptic
     MonTravRes 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 :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(MonTravRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic MonTravRes a b) q s t
-> ExOptic MonTravRes a b s t
ExProstrong @(Rep (Coproduct (UN COPR cx))) @(Corep (Coproduct (UN COPR cx))) (((UN 'COPR a || x) ~> (Coproduct (UN 'COPR a) @ x))
-> Rep (Coproduct (UN 'COPR a)) (UN 'COPR a || x) x
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (UN 'COPR a || x) ~> (Coproduct (UN 'COPR a) @ x)
(UN 'COPR a || x) ~> (UN 'COPR a || x)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Rep (Coproduct (UN 'COPR a)) (UN 'COPR a || x) x
-> ExOptic MonTravRes a b x y
-> (:.:)
     (Rep (Coproduct (UN 'COPR a)))
     (ExOptic MonTravRes a b)
     (UN 'COPR a || x)
     y
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ExOptic MonTravRes a b x y
e (:.:)
  (Rep (Coproduct (UN 'COPR a)))
  (ExOptic MonTravRes a b)
  (UN 'COPR a || x)
  y
-> Corep (Coproduct (UN 'COPR a)) y (UN 'COPR a || y)
-> (:.:)
     (Rep (Coproduct (UN 'COPR a)) :.: ExOptic MonTravRes a b)
     (Corep (Coproduct (UN 'COPR a)))
     (UN 'COPR a || x)
     (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
:.: ((Coproduct (UN 'COPR a) @ y) ~> (UN 'COPR a || y))
-> Corep (Coproduct (UN 'COPR a)) y (UN 'COPR a || y)
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (Coproduct (UN 'COPR a) @ y) ~> (UN 'COPR a || y)
(UN 'COPR a || y) ~> (UN 'COPR a || y)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

-- The free __full-traversal__ profunctor @'ExOptic' 'TravRes'@: like @'ExOptic' 'MonTravRes'@ but
-- additionally carrying product strength (@'Strong' 'ProdAction'@) -- the one thing a
-- lens-as-traversal needs. Instantiating a profunctor-class traversal at this carrier recovers a
-- full 'Traversal' (see 'traversal' below), just as @'ExOptic' 'MonTravRes'@ recovers a
-- 'MonoidalTraversal'. Tensor and coproduct strength reuse the same 'TensorW' and coproduct-prism
-- witnesses as the monoidal-traversal carrier (both are already 'TravRes'); only 'ProdAction' is new,
-- witnessed by the product lens @'Rep' ('Product' _)@.
instance (CopyDiscard k, Ob (a :: k), Ob b) => Strong Tensor (ExOptic TravRes a b :: k +-> k) where
  act :: forall (a :: k) (x :: k) (y :: k).
Ob a =>
ExOptic TravRes a b x y
-> ExOptic TravRes a b (Act Tensor a x) (Act Tensor a y)
act @x @y @z e :: ExOptic TravRes a b x y
e@ExOptic TravRes a b x 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 TravRes a b (Act Tensor a x) (Act Tensor a y))
 -> ExOptic TravRes a b (Act Tensor a x) (Act Tensor a y))
-> (Ob (a ** x) =>
    ExOptic TravRes a b (Act Tensor a x) (Act Tensor a y))
-> ExOptic TravRes 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 TravRes a b (Act Tensor a x) (Act Tensor a y))
 -> ExOptic TravRes a b (Act Tensor a x) (Act Tensor a y))
-> (Ob (a ** y) =>
    ExOptic TravRes a b (Act Tensor a x) (Act Tensor a y))
-> ExOptic TravRes 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 :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(TravRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic TravRes a b) q s t -> ExOptic TravRes a b s t
ExProstrong @(TensorW x) @(CoTensorW x) (((a ** x) ~> (a ** x)) -> TensorW a (a ** x) x
forall {k} (a :: k) (x :: k) (s :: k).
(Ob a, Ob x) =>
(s ~> (a ** x)) -> TensorW a s x
TensorW (a ** x) ~> (a ** x)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id TensorW a (a ** x) x
-> ExOptic TravRes a b x y
-> (:.:) (TensorW a) (ExOptic TravRes a b) (a ** x) y
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ExOptic TravRes a b x y
e (:.:) (TensorW a) (ExOptic TravRes a b) (a ** x) y
-> CoTensorW a y (a ** y)
-> (:.:)
     (TensorW a :.: ExOptic TravRes a b) (CoTensorW a) (a ** x) (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
:.: ((a ** y) ~> (a ** y)) -> CoTensorW a y (a ** y)
forall {k} (a :: k) (x :: k) (t :: k).
(Ob a, Ob x) =>
((a ** x) ~> t) -> CoTensorW a x t
CoTensorW (a ** y) ~> (a ** y)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

instance (HasCoproducts k, CopyDiscard k, Ob (a :: k), Ob b) => Strong CoprodAction (ExOptic TravRes a b :: k +-> k) where
  act :: forall (a :: COPROD k) (x :: k) (y :: k).
Ob a =>
ExOptic TravRes a b x y
-> ExOptic
     TravRes a b (Act CoprodAction a x) (Act CoprodAction a y)
act @cx @y @z e :: ExOptic TravRes a b x y
e@ExOptic TravRes a b x 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 TravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
 -> ExOptic
      TravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
-> (Ob (UN 'COPR a || x) =>
    ExOptic TravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
-> ExOptic
     TravRes 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 TravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
 -> ExOptic
      TravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
-> (Ob (UN 'COPR a || y) =>
    ExOptic TravRes a b (Act CoprodAction a x) (Act CoprodAction a y))
-> ExOptic
     TravRes 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 :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(TravRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic TravRes a b) q s t -> ExOptic TravRes a b s t
ExProstrong @(Rep (Coproduct (UN COPR cx))) @(Corep (Coproduct (UN COPR cx))) (((UN 'COPR a || x) ~> (Coproduct (UN 'COPR a) @ x))
-> Rep (Coproduct (UN 'COPR a)) (UN 'COPR a || x) x
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (UN 'COPR a || x) ~> (Coproduct (UN 'COPR a) @ x)
(UN 'COPR a || x) ~> (UN 'COPR a || x)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Rep (Coproduct (UN 'COPR a)) (UN 'COPR a || x) x
-> ExOptic TravRes a b x y
-> (:.:)
     (Rep (Coproduct (UN 'COPR a)))
     (ExOptic TravRes a b)
     (UN 'COPR a || x)
     y
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ExOptic TravRes a b x y
e (:.:)
  (Rep (Coproduct (UN 'COPR a)))
  (ExOptic TravRes a b)
  (UN 'COPR a || x)
  y
-> Corep (Coproduct (UN 'COPR a)) y (UN 'COPR a || y)
-> (:.:)
     (Rep (Coproduct (UN 'COPR a)) :.: ExOptic TravRes a b)
     (Corep (Coproduct (UN 'COPR a)))
     (UN 'COPR a || x)
     (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
:.: ((Coproduct (UN 'COPR a) @ y) ~> (UN 'COPR a || y))
-> Corep (Coproduct (UN 'COPR a)) y (UN 'COPR a || y)
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (Coproduct (UN 'COPR a) @ y) ~> (UN 'COPR a || y)
(UN 'COPR a || y) ~> (UN 'COPR a || y)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

instance (HasProducts k, Ob (a :: k), Ob b) => Strong ProdAction (ExOptic TravRes a b :: k +-> k) where
  act :: forall (a :: PROD k) (x :: k) (y :: k).
Ob a =>
ExOptic TravRes a b x y
-> ExOptic TravRes a b (Act ProdAction a x) (Act ProdAction a y)
act @px @y @z e :: ExOptic TravRes a b x y
e@ExOptic TravRes a b x 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 TravRes a b (Act ProdAction a x) (Act ProdAction a y))
 -> ExOptic TravRes a b (Act ProdAction a x) (Act ProdAction a y))
-> (Ob (UN 'PR a && x) =>
    ExOptic TravRes a b (Act ProdAction a x) (Act ProdAction a y))
-> ExOptic TravRes 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 TravRes a b (Act ProdAction a x) (Act ProdAction a y))
 -> ExOptic TravRes a b (Act ProdAction a x) (Act ProdAction a y))
-> (Ob (UN 'PR a && y) =>
    ExOptic TravRes a b (Act ProdAction a x) (Act ProdAction a y))
-> ExOptic TravRes 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 :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(TravRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic TravRes a b) q s t -> ExOptic TravRes a b s t
ExProstrong @(Rep (Product (UN PR px))) @(Corep (Product (UN PR px))) (((UN 'PR a && x) ~> (Product (UN 'PR a) @ x))
-> Rep (Product (UN 'PR a)) (UN 'PR a && x) x
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (UN 'PR a && x) ~> (Product (UN 'PR a) @ x)
(UN 'PR a && x) ~> (UN 'PR a && x)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Rep (Product (UN 'PR a)) (UN 'PR a && x) x
-> ExOptic TravRes a b x y
-> (:.:)
     (Rep (Product (UN 'PR a))) (ExOptic TravRes a b) (UN 'PR a && x) y
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ExOptic TravRes a b x y
e (:.:)
  (Rep (Product (UN 'PR a))) (ExOptic TravRes a b) (UN 'PR a && x) y
-> Corep (Product (UN 'PR a)) y (UN 'PR a && y)
-> (:.:)
     (Rep (Product (UN 'PR a)) :.: ExOptic TravRes a b)
     (Corep (Product (UN 'PR a)))
     (UN 'PR a && x)
     (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
:.: ((Product (UN 'PR a) @ y) ~> (UN 'PR a && y))
-> Corep (Product (UN 'PR a)) y (UN 'PR a && y)
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (Product (UN 'PR a) @ y) ~> (UN 'PR a && y)
(UN 'PR a && y) ~> (UN 'PR a && y)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

-- | 'TravRes' copy of 'besideTensor'. Kept as a separate concrete function (rather than
-- generalizing 'besideTensor' over the flavor) to avoid destabilizing the solver.
besideTensorT
  :: forall {k} (a :: k) b s1 t1 s2 t2
   . (Monoidal k, Ob a, Ob b)
  => ExOptic TravRes a b s1 t1 -> ExOptic TravRes a b s2 t2 -> ExOptic TravRes a b (s1 ** s2) (t1 ** t2)
besideTensorT :: forall {k} (a :: k) (b :: k) (s1 :: k) (t1 :: k) (s2 :: k)
       (t2 :: k).
(Monoidal k, Ob a, Ob b) =>
ExOptic TravRes a b s1 t1
-> ExOptic TravRes a b s2 t2
-> ExOptic TravRes a b (s1 ** s2) (t1 ** t2)
besideTensorT ExOptic TravRes a b s1 t1
l ExOptic TravRes a b s2 t2
r =
  ExOptic TravRes a b s1 t1
-> (forall (p :: k +-> k) (q :: k +-> k).
    (TravRes p q, Profunctor p, Profunctor q) =>
    p s1 a -> q b t1 -> ExOptic TravRes a b (s1 ** s2) (t1 ** t2))
-> ExOptic TravRes a b (s1 ** s2) (t1 ** t2)
forall (a :: k) (b :: k) (s :: k) (t :: k) r.
(CategoryOf k, CategoryOf k) =>
ExOptic TravRes a b s t
-> (forall (p :: k +-> k) (q :: k +-> k).
    (TravRes p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall j k (w :: FLAVOR j k) (a :: k) (b :: j) (s :: k) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
ExOptic w a b s t
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
compress ExOptic TravRes a b s1 t1
l \p1 :: p s1 a
p1@p s1 a
Objs q1 :: q b t1
q1@q b t1
Objs ->
    ExOptic TravRes a b s2 t2
-> (forall (p :: k +-> k) (q :: k +-> k).
    (TravRes p q, Profunctor p, Profunctor q) =>
    p s2 a -> q b t2 -> ExOptic TravRes a b (s1 ** s2) (t1 ** t2))
-> ExOptic TravRes a b (s1 ** s2) (t1 ** t2)
forall (a :: k) (b :: k) (s :: k) (t :: k) r.
(CategoryOf k, CategoryOf k) =>
ExOptic TravRes a b s t
-> (forall (p :: k +-> k) (q :: k +-> k).
    (TravRes p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall j k (w :: FLAVOR j k) (a :: k) (b :: j) (s :: k) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
ExOptic w a b s t
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
compress ExOptic TravRes a b s2 t2
r \p2 :: p s2 a
p2@p s2 a
Objs q2 :: q b t2
q2@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 TravRes a b (s1 ** s2) (t1 ** t2))
 -> ExOptic TravRes a b (s1 ** s2) (t1 ** t2))
-> (Ob (s1 ** s2) => ExOptic TravRes a b (s1 ** s2) (t1 ** t2))
-> ExOptic TravRes 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 TravRes a b (s1 ** s2) (t1 ** t2))
 -> ExOptic TravRes a b (s1 ** s2) (t1 ** t2))
-> (Ob (t1 ** t2) => ExOptic TravRes a b (s1 ** s2) (t1 ** t2))
-> ExOptic TravRes a b (s1 ** s2) (t1 ** t2)
forall a b. (a -> b) -> a -> b
$
          (:.:)
  (Beside p p :.: ExOptic TravRes a b)
  (CoBeside q q)
  (s1 ** s2)
  (t1 ** t2)
-> ExOptic TravRes a b (s1 ** s2) (t1 ** t2)
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong (((s1 ** s2) ~> (s1 ** s2))
-> p s1 a -> p s2 a -> Beside p p (s1 ** s2) a
forall {k} (s :: k) (s1 :: k) (s2 :: k) (p1 :: k +-> k) (x :: k)
       (p2 :: k +-> k).
(s ~> (s1 ** s2)) -> p1 s1 x -> p2 s2 x -> Beside p1 p2 s x
Beside (s1 ** s2) ~> (s1 ** s2)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id p s1 a
p1 p s2 a
p2 Beside p p (s1 ** s2) a
-> ExOptic TravRes a b a b
-> (:.:) (Beside p p) (ExOptic TravRes a b) (s1 ** s2) b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic TravRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) (Beside p p) (ExOptic TravRes a b) (s1 ** s2) b
-> CoBeside q q b (t1 ** t2)
-> (:.:)
     (Beside p p :.: ExOptic TravRes a b)
     (CoBeside q q)
     (s1 ** s2)
     (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
-> q b t2
-> ((t1 ** t2) ~> (t1 ** t2))
-> CoBeside q q b (t1 ** t2)
forall {k} (q1 :: k +-> k) (x :: k) (t1 :: k) (q2 :: k +-> k)
       (t2 :: k) (t :: k).
q1 x t1 -> q2 x t2 -> ((t1 ** t2) ~> t) -> CoBeside q1 q2 x t
CoBeside q b t1
q1 q b t2
q2 (t1 ** t2) ~> (t1 ** t2)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

-- | 'TravRes' copy of 'besideSum'.
besideSumT
  :: forall {k} (a :: k) b s1 t1 s2 t2
   . (HasBinaryCoproducts k, Ob a, Ob b)
  => ExOptic TravRes a b s1 t1 -> ExOptic TravRes a b s2 t2 -> ExOptic TravRes a b (s1 || s2) (t1 || t2)
besideSumT :: forall {k} (a :: k) (b :: k) (s1 :: k) (t1 :: k) (s2 :: k)
       (t2 :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
ExOptic TravRes a b s1 t1
-> ExOptic TravRes a b s2 t2
-> ExOptic TravRes a b (s1 || s2) (t1 || t2)
besideSumT ExOptic TravRes a b s1 t1
l ExOptic TravRes a b s2 t2
r =
  ExOptic TravRes a b s1 t1
-> (forall (p :: k +-> k) (q :: k +-> k).
    (TravRes p q, Profunctor p, Profunctor q) =>
    p s1 a -> q b t1 -> ExOptic TravRes a b (s1 || s2) (t1 || t2))
-> ExOptic TravRes a b (s1 || s2) (t1 || t2)
forall (a :: k) (b :: k) (s :: k) (t :: k) r.
(CategoryOf k, CategoryOf k) =>
ExOptic TravRes a b s t
-> (forall (p :: k +-> k) (q :: k +-> k).
    (TravRes p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall j k (w :: FLAVOR j k) (a :: k) (b :: j) (s :: k) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
ExOptic w a b s t
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
compress ExOptic TravRes a b s1 t1
l \p1 :: p s1 a
p1@p s1 a
Objs q1 :: q b t1
q1@q b t1
Objs ->
    ExOptic TravRes a b s2 t2
-> (forall (p :: k +-> k) (q :: k +-> k).
    (TravRes p q, Profunctor p, Profunctor q) =>
    p s2 a -> q b t2 -> ExOptic TravRes a b (s1 || s2) (t1 || t2))
-> ExOptic TravRes a b (s1 || s2) (t1 || t2)
forall (a :: k) (b :: k) (s :: k) (t :: k) r.
(CategoryOf k, CategoryOf k) =>
ExOptic TravRes a b s t
-> (forall (p :: k +-> k) (q :: k +-> k).
    (TravRes p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall j k (w :: FLAVOR j k) (a :: k) (b :: j) (s :: k) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
ExOptic w a b s t
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
compress ExOptic TravRes a b s2 t2
r \p2 :: p s2 a
p2@p s2 a
Objs q2 :: q b t2
q2@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 TravRes a b (s1 || s2) (t1 || t2))
 -> ExOptic TravRes a b (s1 || s2) (t1 || t2))
-> (Ob (s1 || s2) => ExOptic TravRes a b (s1 || s2) (t1 || t2))
-> ExOptic TravRes 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 TravRes a b (s1 || s2) (t1 || t2))
 -> ExOptic TravRes a b (s1 || s2) (t1 || t2))
-> (Ob (t1 || t2) => ExOptic TravRes a b (s1 || s2) (t1 || t2))
-> ExOptic TravRes a b (s1 || s2) (t1 || t2)
forall a b. (a -> b) -> a -> b
$
          (:.:)
  (BesideSum p p :.: ExOptic TravRes a b)
  (CoBesideSum q q)
  (s1 || s2)
  (t1 || t2)
-> ExOptic TravRes a b (s1 || s2) (t1 || t2)
forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong (((s1 || s2) ~> (s1 || s2))
-> p s1 a -> p s2 a -> BesideSum p p (s1 || s2) a
forall {k} (s :: k) (s1 :: k) (s2 :: k) (p1 :: k +-> k) (x :: k)
       (p2 :: k +-> k).
(s ~> (s1 || s2)) -> p1 s1 x -> p2 s2 x -> BesideSum p1 p2 s x
BesideSum (s1 || s2) ~> (s1 || s2)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id p s1 a
p1 p s2 a
p2 BesideSum p p (s1 || s2) a
-> ExOptic TravRes a b a b
-> (:.:) (BesideSum p p) (ExOptic TravRes a b) (s1 || s2) b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic TravRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) (BesideSum p p) (ExOptic TravRes a b) (s1 || s2) b
-> CoBesideSum q q b (t1 || t2)
-> (:.:)
     (BesideSum p p :.: ExOptic TravRes a b)
     (CoBesideSum q q)
     (s1 || s2)
     (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
-> q b t2
-> ((t1 || t2) ~> (t1 || t2))
-> CoBesideSum q q b (t1 || t2)
forall {k} (q1 :: k +-> k) (x :: k) (t1 :: k) (q2 :: k +-> k)
       (t2 :: k) (t :: k).
q1 x t1 -> q2 x t2 -> ((t1 || t2) ~> t) -> CoBesideSum q1 q2 x t
CoBesideSum q b t1
q1 q b t2
q2 (t1 || t2) ~> (t1 || t2)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

instance (Monoidal k, Ob (a :: k), Ob b) => MonoidalProfunctor (ExOptic TravRes a b :: k +-> k) where
  one :: ExOptic TravRes a b Unit Unit
one = (:.:) (UnitW :.: ExOptic TravRes a b) CoUnitW Unit Unit
-> ExOptic TravRes 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 :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong ((Unit ~> Unit) -> UnitW Unit a
forall {k} (x :: k) (s :: k). Ob x => (s ~> Unit) -> UnitW s x
UnitW Unit ~> Unit
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id UnitW Unit a
-> ExOptic TravRes a b a b
-> (:.:) UnitW (ExOptic TravRes a b) Unit b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic TravRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) UnitW (ExOptic TravRes a b) Unit b
-> CoUnitW b Unit
-> (:.:) (UnitW :.: ExOptic TravRes a b) CoUnitW Unit Unit
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) -> 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  ExOptic TravRes a b x1 x2
l ** :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
ExOptic TravRes a b x1 x2
-> ExOptic TravRes a b y1 y2
-> ExOptic TravRes a b (x1 ** y1) (x2 ** y2)
** ExOptic TravRes a b y1 y2
r = ExOptic TravRes a b x1 x2
-> ExOptic TravRes a b y1 y2
-> ExOptic TravRes a b (x1 ** y1) (x2 ** y2)
forall {k} (a :: k) (b :: k) (s1 :: k) (t1 :: k) (s2 :: k)
       (t2 :: k).
(Monoidal k, Ob a, Ob b) =>
ExOptic TravRes a b s1 t1
-> ExOptic TravRes a b s2 t2
-> ExOptic TravRes a b (s1 ** s2) (t1 ** t2)
besideTensorT ExOptic TravRes a b x1 x2
l ExOptic TravRes a b y1 y2
r

instance (HasCoproducts k, Ob (a :: k), Ob b) => MonoidalProfunctor (Coprod (ExOptic TravRes a b :: k +-> k)) where
  one :: Coprod (ExOptic TravRes a b) Unit Unit
one = ExOptic TravRes a b InitialObject InitialObject
-> Coprod
     (ExOptic TravRes 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 :.: ExOptic TravRes a b) CoZeroW InitialObject InitialObject
-> ExOptic TravRes 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 :.: ExOptic w a b) q s t -> ExOptic w a b s t
ExProstrong ((InitialObject ~> InitialObject) -> ZeroW InitialObject a
forall {k} (x :: k) (s :: k).
Ob x =>
(s ~> InitialObject) -> ZeroW s x
ZeroW InitialObject ~> InitialObject
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id ZeroW InitialObject a
-> ExOptic TravRes a b a b
-> (:.:) ZeroW (ExOptic TravRes a b) InitialObject b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic TravRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) ZeroW (ExOptic TravRes a b) InitialObject b
-> CoZeroW b InitialObject
-> (:.:)
     (ZeroW :.: ExOptic TravRes a b) CoZeroW InitialObject InitialObject
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) -> 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id))
  Coprod ExOptic TravRes a b a1 b1
l ** :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod (ExOptic TravRes a b) x1 x2
-> Coprod (ExOptic TravRes a b) y1 y2
-> Coprod (ExOptic TravRes a b) (x1 ** y1) (x2 ** y2)
** Coprod ExOptic TravRes a b a1 b1
r = ExOptic TravRes a b (a1 || a1) (b1 || b1)
-> Coprod
     (ExOptic TravRes 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 TravRes a b a1 b1
-> ExOptic TravRes a b a1 b1
-> ExOptic TravRes a b (a1 || a1) (b1 || b1)
forall {k} (a :: k) (b :: k) (s1 :: k) (t1 :: k) (s2 :: k)
       (t2 :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
ExOptic TravRes a b s1 t1
-> ExOptic TravRes a b s2 t2
-> ExOptic TravRes a b (s1 || s2) (t1 || t2)
besideSumT ExOptic TravRes a b a1 b1
l ExOptic TravRes a b a1 b1
r)

-- | The other half of the equivalence between the encodings: instantiate the
-- profunctor-class-flavored traversal at the free __monoidal-traversal__ profunctor
-- @'ExOptic' 'MonTravRes'@. Because that carrier's 'Proarrow.Category.Monoidal.Strength.MonStrong'
-- instance uses the tensor-strength witness 'TensorW' (not a product lens), this needs no
-- 'Proarrow.Limit.BinaryProduct.Cartesian' (@tensor = product@), only 'Proarrow.Category.Monoidal.CopyDiscard.CopyDiscard' (a discard @a '~>' 'Unit' for the residual) -- which is
-- exactly what the coproduct-prism side (@'Strong' 'CoprodAction' ('ExOptic' 'MonTravRes')@) already
-- demanded, so no constraint is added beyond relaxing 'Proarrow.Limit.BinaryProduct.Cartesian' to 'CopyDiscard' -- enabling e.g.
-- the biproduct categories @Mat@ and @FinRel@ (but not @LINEAR@, which cannot discard). A 'Traversal'
-- is recovered for free wherever one is needed, since @'MonTravRes'@ is a 'SubFlavor' of 'TravRes'.
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 MonTravRes) 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, (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.
monTraverseOf
  :: forall {k} w (s :: k) (t :: k) a b p
   . (Distributive k, StrongDistributiveProfunctor p, SubFlavor w MonTravRes)
  => Optic (Prostrong w) s t a b -> p a b -> p s t
monTraverseOf :: forall {k} (w :: FLAVOR k k) (s :: k) (t :: k) (a :: k) (b :: k)
       (p :: k +-> k).
(Distributive k, StrongDistributiveProfunctor p,
 SubFlavor w MonTravRes) =>
Optic (Prostrong w) s t a b -> p a b -> p s t
monTraverseOf Optic (Prostrong w) s t a b
o p a b
pab = (forall (p :: k +-> k) (q :: k +-> k).
 (MonTravRes p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> p s t)
-> Optic (Prostrong MonTravRes) s t a b -> p s t
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs (\p s a
l q b t
r -> p s a -> q b t -> p a b -> p s t
forall {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
p s a -> q b t -> r a b -> r s t
monTravP p s a
l q b t
r p a b
pab) (forall {j} {k} (c :: (k -> j -> Type) -> Constraint)
       (w :: FLAVOR j k) (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b -> Optic (Prostrong w) s t a b
forall (c :: (k +-> k) -> Constraint) (w :: FLAVOR k k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b -> Optic (Prostrong w) s t a b
convert @(Prostrong w) @MonTravRes Optic (Prostrong w) s t a b
o)

instance IsOptic StrongDistributiveProfunctor where withProfunctor :: forall (p :: j +-> j) r.
StrongDistributiveProfunctor p =>
(Profunctor p => r) -> r
withProfunctor Profunctor p => r
r = r
Profunctor p => r
r

-- | 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 = (forall (p :: k +-> k) (q :: k +-> k).
 (MonTravRes p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> PTraversal s t a b)
-> Optic (Prostrong MonTravRes) s t a b -> PTraversal s t a b
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs \l :: p s a
l@p s a
Objs r :: q b t
r@q b t
Objs -> (forall (p :: k +-> k).
 StrongDistributiveProfunctor 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 => 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).
(MonTravRes p q, StrongDistributiveProfunctor r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
p s a -> q b t -> r a b -> r s t
monTravP 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 -- exactly 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 van-Laarhoven \/ profunctor-class form, by instantiating the
-- rank-2 function at the free full-traversal profunctor @'ExOptic' 'TravRes'@ (an
-- 'StrongDistributiveProfunctor' /and/ @'Strong' 'ProdAction'@, unlike @'ExOptic' 'MonTravRes'@).
-- 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 = ExOptic TravRes a b s t -> Optic (Prostrong TravRes) s t a b
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof (ExOptic TravRes a b a b -> ExOptic TravRes a b s t
forall (r :: k +-> k).
(StrongDistributiveProfunctor r, Strong ProdAction r) =>
r a b -> r s t
f ((a ~> a) -> (b ~> b) -> ExOptic TravRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id))

-- | 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 = (forall (p :: k +-> k) (q :: k +-> k).
 (TravRes p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> PTraversalFull s t a b)
-> Optic (Prostrong TravRes) s t a b -> PTraversalFull s t a b
forall j k (w :: FLAVOR j k) (s :: k) (a :: k) (b :: j) (t :: j) r.
(CompactFlavor w, CategoryOf j, CategoryOf k) =>
(forall (p :: k +-> k) (q :: j +-> j).
 (w p q, Profunctor p, Profunctor q) =>
 p s a -> q b t -> r)
-> Optic (Prostrong w) s t a b -> r
withLegs \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 =>
 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 => 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).
(TravRes p q, StrongDistributiveProfunctor r,
 Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
(StrongDistributiveProfunctor r, Strong ProdAction r) =>
p s a -> q b t -> r a b -> r s t
travP p s a
l q b t
r)

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 =>
 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 => 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 =>
 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 => 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 =>
 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 => 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 =>
p a b -> p s t
l) = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor 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 => 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 =>
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 =>
p a b -> p s t
l) = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor 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 => 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 =>
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 =>
 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 => 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 =>
p a b -> p s t
l) (Optic forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
r) = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor 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 => 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 =>
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 =>
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 =>
p a b -> p s t
l) (Optic forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
r) = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor 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 => 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 =>
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 =>
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 =>
p a b -> p s t
l) (Optic forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
r) = (forall (p :: Type +-> Type).
 StrongDistributiveProfunctor 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 => 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 =>
p a b -> p s t
l (p a b -> p s t
forall (p :: Type +-> Type).
StrongDistributiveProfunctor p =>
p a b -> p s t
r p a a'
p a b
p))