{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE IncoherentInstances #-}
{-# OPTIONS_GHC -Wno-orphans -fprint-potential-instances #-}

module Proarrow.Category.Monoidal.Optic where

import Data.Bifunctor (bimap)
import Data.Kind (Type)
import GHC.Generics qualified as G
import Prelude (Either (..), Maybe (..), Monad (..), Traversable, const, either, fmap, uncurry, ($))

import Data.Monoid qualified as P
import Proarrow.Category.Instance.Kleisli (KLEISLI (..), Kleisli (..))
import Proarrow.Category.Instance.Nat ((!))
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal, obj2, swap)
import Proarrow.Category.Monoidal.Action
  ( Costrong (..)
  , MonoidalAction (..)
  , SelfAction
  , Strong (..)
  , composeActs
  , decomposeActs
  , fromSelfAct
  , strongPar0
  )
import Proarrow.Category.Monoidal.Distributive qualified as Dist
import Proarrow.Core
  ( Any
  , CAT
  , CategoryOf (..)
  , Kind
  , OB
  , Profunctor (..)
  , Promonad (..)
  , UN
  , obj
  , rmap
  , (//)
  , type (+->)
  )
import Proarrow.Functor (Prelude (..))
import Proarrow.Object (src, tgt)
import Proarrow.Object.BinaryCoproduct
  ( COPROD (..)
  , Coprod (..)
  , HasBinaryCoproducts (..)
  , HasCoproducts
  , copar
  , copar0
  )
import Proarrow.Object.BinaryProduct (Cartesian, HasBinaryProducts (..), HasProducts, PROD, Prod (..))
import Proarrow.Optic (InvertableOptic, Optic, Optic_ (..), Re (..))
import Proarrow.Profunctor.Constant (Constant)
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..), Representable (..), withRepOb)
import Proarrow.Profunctor.Star (Star, pattern Star)

type ExOptic :: Kind -> c -> d -> c -> d -> Type
data ExOptic m a b s t where
  ExOptic
    :: forall {c} {d} {m} (x :: m) (x' :: m) a b s t
     . (Ob (a :: c), Ob (b :: d))
    => s ~> (x `Act` a)
    -> x ~> x'
    -> (x' `Act` b) ~> t
    -> ExOptic m a b s t

type IsOptic m c d = (MonoidalAction m c, MonoidalAction m d)

instance (CategoryOf c, CategoryOf d) => Profunctor (ExOptic m a b :: c +-> d) where
  dimap :: forall (c :: d) (a :: d) (b :: c) (d :: c).
(c ~> a) -> (b ~> d) -> ExOptic m a b a b -> ExOptic m a b c d
dimap c ~> a
l b ~> d
r (ExOptic a ~> Act x a
f x ~> x'
w Act x' b ~> b
g) = (c ~> Act x a) -> (x ~> x') -> (Act x' b ~> d) -> ExOptic m a b c d
forall {c} {d} {m} (b :: m) (t :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act b a) -> (b ~> t) -> (Act t b ~> t) -> ExOptic m a b s t
ExOptic (a ~> Act x a
f (a ~> Act x a) -> (c ~> a) -> c ~> Act x a
forall (b :: d) (c :: d) (a :: d). (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) x ~> x'
w (b ~> d
r (b ~> d) -> (Act x' b ~> b) -> Act x' b ~> d
forall (b :: c) (c :: c) (a :: c). (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
. Act x' b ~> b
g)
  (Ob a, Ob b) => r
r \\ :: forall (a :: d) (b :: c) r.
((Ob a, Ob b) => r) -> ExOptic m a b a b -> r
\\ ExOptic a ~> Act x a
f x ~> x'
_ Act x' b ~> b
g = r
(Ob a, Ob b) => r
(Ob a, Ob (Act x a)) => r
r ((Ob a, Ob (Act x a)) => r) -> (a ~> Act x a) -> r
forall (a :: d) (b :: d) 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 ~> Act x a
f ((Ob (Act x' b), Ob b) => r) -> (Act x' b ~> b) -> r
forall (a :: c) (b :: c) 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
\\ Act x' b ~> b
g

instance (IsOptic m c d) => Strong m (ExOptic m a b :: c +-> d) where
  act
    :: forall (a1 :: m) (b1 :: m) (s :: d) (t :: c). a1 ~> b1 -> ExOptic m a b s t -> ExOptic m a b (Act a1 s) (Act b1 t)
  act :: forall (a :: m) (b :: m) (x :: d) (y :: c).
(a ~> b) -> ExOptic m a b x y -> ExOptic m a b (Act a x) (Act b y)
act a1 ~> b1
w (ExOptic @x @x' s ~> Act x a
f x ~> x'
w' Act x' b ~> t
g) =
    (Act a1 s ~> Act (a1 ** x) a)
-> ((a1 ** x) ~> (b1 ** x'))
-> (Act (b1 ** x') b ~> Act b1 t)
-> ExOptic m a b (Act a1 s) (Act b1 t)
forall {c} {d} {m} (b :: m) (t :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act b a) -> (b ~> t) -> (Act t b ~> t) -> ExOptic m a b s t
ExOptic (forall (x :: m) (y :: m) (c :: d) (a :: d) (b :: d).
(MonoidalAction m d, Ob x, Ob y, Ob c) =>
(a ~> Act x b) -> (b ~> Act y c) -> a ~> Act (x ** y) c
forall {m} {k} (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(a ~> Act x b) -> (b ~> Act y c) -> a ~> Act (x ** y) c
composeActs @a1 @x @a ((a1 ~> b1) -> a1 ~> a1
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src a1 ~> b1
w (a1 ~> a1) -> (s ~> s) -> Act a1 s ~> Act a1 s
forall (a :: m) (b :: m) (x :: d) (y :: d).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` (s ~> Act x a) -> s ~> s
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src s ~> Act x a
f) s ~> Act x a
f) (a1 ~> b1
w (a1 ~> b1) -> (x ~> x') -> (a1 ** x) ~> (b1 ** x')
forall (x1 :: m) (x2 :: m) (y1 :: m) (y2 :: m).
(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)
`par` x ~> x'
w') (forall (x :: m) (y :: m) (c :: c) (a :: c) (b :: c).
(MonoidalAction m c, Ob x, Ob y, Ob c) =>
(Act y c ~> b) -> (Act x b ~> a) -> Act (x ** y) c ~> a
forall {m} {k} (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(Act y c ~> b) -> (Act x b ~> a) -> Act (x ** y) c ~> a
decomposeActs @b1 @x' @b Act x' b ~> t
g ((a1 ~> b1) -> b1 ~> b1
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt a1 ~> b1
w (b1 ~> b1) -> (t ~> t) -> Act b1 t ~> Act b1 t
forall (a :: m) (b :: m) (x :: c) (y :: c).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` (Act x' b ~> t) -> t ~> t
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt Act x' b ~> t
g))
      ((Ob a1, Ob b1) => ExOptic m a b (Act a1 s) (Act b1 t))
-> (a1 ~> b1) -> ExOptic m a b (Act a1 s) (Act b1 t)
forall (a :: m) (b :: m) 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
\\ a1 ~> b1
w
      ((Ob x, Ob x') => ExOptic m a b (Act a1 s) (Act b1 t))
-> (x ~> x') -> ExOptic m a b (Act a1 s) (Act b1 t)
forall (a :: m) (b :: m) 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
\\ x ~> x'
w'

ex2prof
  :: forall {c} {d} m (a :: c) (b :: d) s t. (CategoryOf c, CategoryOf d) => ExOptic m a b s t -> Optic (Strong m) s t a b
ex2prof :: forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d).
(CategoryOf c, CategoryOf d) =>
ExOptic m a b s t -> Optic (Strong m) s t a b
ex2prof (ExOptic s ~> Act x a
l x ~> x'
w Act x' b ~> t
r) = (forall (p :: d +-> c). Strong m p => p a b -> p s t)
-> Optic (Strong m) 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 ((s ~> Act x a)
-> (Act x' b ~> t) -> p (Act x a) (Act x' b) -> p s t
forall (c :: c) (a :: c) (b :: d) (d :: 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 s ~> Act x a
l Act x' b ~> t
r (p (Act x a) (Act x' b) -> p s t)
-> (p a b -> p (Act x a) (Act x' b)) -> p a b -> p s t
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x ~> x') -> p a b -> p (Act x a) (Act x' b)
forall (a :: m) (b :: m) (x :: c) (y :: d).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act x ~> x'
w) ((Ob s, Ob (Act x a)) => Optic (Strong m) s t a b)
-> (s ~> Act x a) -> Optic (Strong m) s t a b
forall (a :: c) (b :: c) 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
\\ s ~> Act x a
l ((Ob (Act x' b), Ob t) => Optic (Strong m) s t a b)
-> (Act x' b ~> t) -> Optic (Strong m) s t a b
forall (a :: d) (b :: d) 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
\\ Act x' b ~> t
r

prof2ex
  :: forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d)
   . (IsOptic m c d, Ob a, Ob b)
  => Optic (Strong m) s t a b
  -> ExOptic m a b s t
prof2ex :: forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d).
(IsOptic m c d, Ob a, Ob b) =>
Optic (Strong m) s t a b -> ExOptic m a b s t
prof2ex Optic (Strong m) s t a b
p2p = Optic (Strong m) s t a b
-> forall (p :: d +-> c). Strong m p => p a b -> p s t
forall k (a :: k) j (b :: j) (s :: k) (t :: j)
       (c :: (j +-> k) -> Constraint).
Optic_ (OPT a b) (OPT s t)
-> forall (p :: j +-> k). c p => p a b -> p s t
over Optic (Strong m) s t a b
p2p ((a ~> Act Unit a)
-> (Unit ~> Unit) -> (Act Unit b ~> b) -> ExOptic m a b a b
forall {c} {d} {m} (b :: m) (t :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act b a) -> (b ~> t) -> (Act t b ~> t) -> ExOptic m a b s t
ExOptic (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m) Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 (forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m))

type MonoidalOptic (s :: k) (t :: k) a b = Optic (Strong (SUBCAT (Any :: OB k))) s t a b
mkMonoidal
  :: forall {k} (m :: k) (a :: k) (b :: k) s t
   . (Monoidal k, Ob m, Ob a, Ob b) => (s ~> m ** a) -> (m ** b ~> t) -> MonoidalOptic s t a b
mkMonoidal :: forall {k} (m :: k) (a :: k) (b :: k) (s :: k) (t :: k).
(Monoidal k, Ob m, Ob a, Ob b) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalOptic s t a b
mkMonoidal s ~> (m ** a)
sma (m ** b) ~> t
mbt = ExOptic (SUBCAT Any) a b s t -> Optic (Strong (SUBCAT Any)) s t a b
forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d).
(CategoryOf c, CategoryOf d) =>
ExOptic m a b s t -> Optic (Strong m) s t a b
ex2prof ((s ~> Act (SUB m) a)
-> (SUB m ~> SUB m)
-> (Act (SUB m) b ~> t)
-> ExOptic (SUBCAT Any) a b s t
forall {c} {d} {m} (b :: m) (t :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act b a) -> (b ~> t) -> (Act t b ~> t) -> ExOptic m a b s t
ExOptic s ~> (m ** a)
s ~> Act (SUB m) a
sma (forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
forall (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub @(Any :: OB k) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m)) (m ** b) ~> t
Act (SUB m) b ~> t
mbt)

_1 :: forall {k} (a :: k) b c. (SymMonoidal k, Ob a, Ob b, Ob c) => MonoidalOptic (a ** c) (b ** c) a b
_1 :: forall {k} (a :: k) (b :: k) (c :: k).
(SymMonoidal k, Ob a, Ob b, Ob c) =>
MonoidalOptic (a ** c) (b ** c) a b
_1 = forall (m :: k) (a :: k) (b :: k) (s :: k) (t :: k).
(Monoidal k, Ob m, Ob a, Ob b) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalOptic s t a b
forall {k} (m :: k) (a :: k) (b :: k) (s :: k) (t :: k).
(Monoidal k, Ob m, Ob a, Ob b) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalOptic s t a b
mkMonoidal @c (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @c) (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @c @b)

_2 :: forall {k} (a :: k) b c. (SymMonoidal k, Ob a, Ob b, Ob c) => MonoidalOptic (c ** a) (c ** b) a b
_2 :: forall {k} (a :: k) (b :: k) (c :: k).
(SymMonoidal k, Ob a, Ob b, Ob c) =>
MonoidalOptic (c ** a) (c ** b) a b
_2 = forall (m :: k) (a :: k) (b :: k) (s :: k) (t :: k).
(Monoidal k, Ob m, Ob a, Ob b) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalOptic s t a b
forall {k} (m :: k) (a :: k) (b :: k) (s :: k) (t :: k).
(Monoidal k, Ob m, Ob a, Ob b) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalOptic s t a b
mkMonoidal @c (forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @c @a) (forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @c @b)

instance
  (Cartesian k, Ob c, Strong (SUBCAT (Any :: OB k)) ((~>) :: CAT k))
  => Strong (SUBCAT (Any :: OB k)) (Rep (Constant c) :: k +-> k)
  where
  act :: forall (a :: SUBCAT Any) (b :: SUBCAT Any) (x :: k) (y :: k).
(a ~> b)
-> Rep (Constant c) x y -> Rep (Constant c) (Act a x) (Act b y)
act @m @m' @x @y a ~> b
g (Rep x ~> (Constant c @ y)
f) = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @(UN SUB m') @y (((UN SUB a ** x) ~> (Constant c @ (UN SUB b ** y)))
-> Rep (Constant c) (UN SUB a ** x) (UN SUB b ** y)
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (x ~> c
x ~> (Constant c @ y)
f (x ~> c) -> ((UN SUB a ** x) ~> x) -> (UN SUB a ** x) ~> c
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) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @(UN SUB m) @x)) ((Ob a, Ob b) => Rep (Constant c) (UN SUB a ** x) (UN SUB b ** y))
-> Sub (~>) a b -> Rep (Constant c) (UN SUB a ** x) (UN SUB b ** y)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: SUBCAT Any) (b :: SUBCAT Any) r.
((Ob a, Ob b) => r) -> Sub (~>) a b -> r
\\ a ~> b
Sub (~>) a b
g ((Ob x, Ob c) => Rep (Constant c) (UN SUB a ** x) (UN SUB b ** y))
-> (x ~> c) -> Rep (Constant c) (UN SUB a ** x) (UN SUB b ** y)
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
\\ x ~> c
x ~> (Constant c @ y)
f
instance (Cartesian k, SelfAction k, Ob c) => Strong k (Rep (Constant c) :: k +-> k) where
  act :: forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b)
-> Rep (Constant c) x y -> Rep (Constant c) (Act a x) (Act b y)
act @m @m' @x @y a ~> b
g (Rep x ~> (Constant c @ y)
f) = forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @k @k @m' @y ((Act a x ~> (Constant c @ Act b y))
-> Rep (Constant c) (Act a x) (Act b y)
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (x ~> c
x ~> (Constant c @ y)
f (x ~> c) -> (Act a x ~> x) -> Act a x ~> c
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) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @m @x ((a && x) ~> x) -> (Act a x ~> (a && x)) -> Act a x ~> x
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) (b :: k).
(SelfAction k, Ob a, Ob b) =>
Act a b ~> (a ** b)
forall {k} (a :: k) (b :: k).
(SelfAction k, Ob a, Ob b) =>
Act a b ~> (a ** b)
fromSelfAct @m @x)) ((Ob a, Ob b) => Rep (Constant c) (Act a x) (Act b y))
-> (a ~> b) -> Rep (Constant c) (Act a x) (Act b y)
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 ~> b
g ((Ob x, Ob c) => Rep (Constant c) (Act a x) (Act b y))
-> (x ~> c) -> Rep (Constant c) (Act a x) (Act b y)
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
\\ x ~> c
x ~> (Constant c @ y)
f
instance Strong (COPROD Type) (Rep (Constant (P.First c)) :: Type +-> Type) where
  act :: forall (a :: COPROD Type) (b :: COPROD Type) x y.
(a ~> b)
-> Rep (Constant (First c)) x y
-> Rep (Constant (First c)) (Act a x) (Act b y)
act a ~> b
_ (Rep x ~> (Constant (First c) @ y)
f) = (Either (UN 'COPR a) x
 ~> (Constant (First c) @ Either (UN 'COPR b) y))
-> Rep
     (Constant (First c))
     (Either (UN 'COPR a) x)
     (Either (UN 'COPR b) y)
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep ((UN 'COPR a -> First c)
-> (x -> First c) -> Either (UN 'COPR a) x -> First c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (First c -> UN 'COPR a -> First c
forall a b. a -> b -> a
const (Maybe c -> First c
forall a. Maybe a -> First a
P.First Maybe c
forall a. Maybe a
Nothing)) x ~> (Constant (First c) @ y)
x -> First c
f)

type Lens (s :: k) (t :: k) a b = Optic (Strong (PROD k)) s t a b
mkLens :: forall {k} (s :: k) (t :: k) a b. (HasProducts k, Ob b) => (s ~> a) -> ((s && b) ~> t) -> Lens s t a b
mkLens :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(HasProducts k, Ob b) =>
(s ~> a) -> ((s && b) ~> t) -> Lens s t a b
mkLens s ~> a
sa (s && b) ~> t
sbt = ExOptic (PROD k) a b s t -> Optic (Strong (PROD k)) s t a b
forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d).
(CategoryOf c, CategoryOf d) =>
ExOptic m a b s t -> Optic (Strong m) s t a b
ex2prof ((s ~> Act ('PR s) a)
-> ('PR s ~> 'PR s)
-> (Act ('PR s) b ~> t)
-> ExOptic (PROD k) a b s t
forall {c} {d} {m} (b :: m) (t :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act b a) -> (b ~> t) -> (Act t b ~> t) -> ExOptic m a b s t
ExOptic (s ~> s
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (s ~> s) -> (s ~> a) -> s ~> (s && a)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& s ~> a
sa) ((s ~> s) -> Prod (~>) ('PR s) ('PR s)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod ((s ~> a) -> s ~> s
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src s ~> a
sa)) Act ('PR s) b ~> t
(s && b) ~> t
sbt) ((Ob s, Ob a) => Optic (Strong (PROD k)) s t a b)
-> (s ~> a) -> Optic (Strong (PROD k)) s t a b
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
\\ s ~> a
sa

type Prism (s :: k) t a b = Optic (Strong (COPROD k)) s t a b
mkPrism :: forall {k} (s :: k) (t :: k) a b. (HasCoproducts k, Ob a) => (s ~> (t || a)) -> (b ~> t) -> Prism s t a b
mkPrism :: forall {k} (s :: k) (t :: k) (a :: k) (b :: k).
(HasCoproducts k, Ob a) =>
(s ~> (t || a)) -> (b ~> t) -> Prism s t a b
mkPrism s ~> (t || a)
sta b ~> t
bt = ExOptic (COPROD k) a b s t -> Optic (Strong (COPROD k)) s t a b
forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d).
(CategoryOf c, CategoryOf d) =>
ExOptic m a b s t -> Optic (Strong m) s t a b
ex2prof ((s ~> Act ('COPR t) a)
-> ('COPR t ~> 'COPR t)
-> (Act ('COPR t) b ~> t)
-> ExOptic (COPROD k) a b s t
forall {c} {d} {m} (b :: m) (t :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act b a) -> (b ~> t) -> (Act t b ~> t) -> ExOptic m a b s t
ExOptic s ~> Act ('COPR t) a
s ~> (t || a)
sta (Id t t -> Coprod Id ('COPR t) ('COPR t)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod ((t ~> t) -> Id t t
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((b ~> t) -> t ~> t
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt b ~> t
bt))) (t ~> t
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (t ~> t) -> (b ~> t) -> (t || b) ~> t
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| b ~> t
bt)) ((Ob b, Ob t) => Optic (Strong (COPROD k)) s t a b)
-> (b ~> t) -> Optic (Strong (COPROD k)) s t a b
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 ~> t
bt

type HaskTraversal s t a b = Optic (Strong (SUBCAT Traversable)) s t a b
traversing :: (Traversable f) => HaskTraversal (f a) (f b) a b
traversing :: forall (f :: Type -> Type) a b.
Traversable f =>
HaskTraversal (f a) (f b) a b
traversing = forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d).
(CategoryOf c, CategoryOf d) =>
ExOptic m a b s t -> Optic (Strong m) s t a b
forall m a b s t.
(CategoryOf Type, CategoryOf Type) =>
ExOptic m a b s t -> Optic (Strong m) s t a b
ex2prof @(SUBCAT Traversable) ((f a ~> Act (SUB (Prelude f)) a)
-> (SUB (Prelude f) ~> SUB (Prelude f))
-> (Act (SUB (Prelude f)) b ~> f b)
-> ExOptic (SUBCAT Traversable) a b (f a) (f b)
forall {c} {d} {m} (b :: m) (t :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act b a) -> (b ~> t) -> (Act t b ~> t) -> ExOptic m a b s t
ExOptic f a ~> Act (SUB (Prelude f)) a
f a -> Prelude f a
forall (f :: Type -> Type) a. f a -> Prelude f a
Prelude SUB (Prelude f) ~> SUB (Prelude f)
Sub Nat (SUB (Prelude f)) (SUB (Prelude f))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SUBCAT Traversable). Ob a => Sub Nat a a
id Act (SUB (Prelude f)) b ~> f b
Prelude f b -> f b
forall (f :: Type -> Type) a. Prelude f a -> f a
unPrelude)

type Traversal s t a b = Optic Dist.StrongDistributiveProfunctor s t a b
traversing' :: forall t a b. (Dist.Traversable t, Representable t, Ob a, Ob b) => Traversal (t % a) (t % b) a b
traversing' :: forall {j} (t :: j +-> j) (a :: j) (b :: j).
(Traversable t, Representable t, Ob a, Ob b) =>
Traversal (t % a) (t % b) a b
traversing' = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> j) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepOb @t @a ((Ob (t % a) => Traversal (t % a) (t % b) a b)
 -> Traversal (t % a) (t % b) a b)
-> (Ob (t % a) => Traversal (t % a) (t % b) a b)
-> Traversal (t % a) (t % b) a b
forall a b. (a -> b) -> a -> b
$ forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: j +-> j) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepOb @t @b ((Ob (t % b) => Traversal (t % a) (t % b) a b)
 -> Traversal (t % a) (t % b) a b)
-> (Ob (t % b) => Traversal (t % a) (t % b) a b)
-> Traversal (t % a) (t % b) a b
forall a b. (a -> b) -> a -> b
$ (forall (p :: j +-> j).
 StrongDistributiveProfunctor p =>
 p a b -> p (t % a) (t % b))
-> Traversal (t % a) (t % b) 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 (forall {k} (t :: k +-> k) (p :: k +-> k) (a :: k) (b :: k).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
forall (t :: j +-> j) (p :: j +-> j) (a :: j) (b :: j).
(Traversable t, Representable t, StrongDistributiveProfunctor p) =>
p a b -> p (t % a) (t % b)
Dist.repTraverse @t)

class (Monad m) => Algebra m a where algebra :: m a -> a
instance (Monad m) => Algebra m (m a) where algebra :: m (m a) -> m a
algebra = (m (m a) -> (m a -> m a) -> m a
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= m a -> m a
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
instance (Monad m) => Algebra m () where algebra :: m () -> ()
algebra m ()
_ = ()
instance (Monad m, Algebra m a, Algebra m b) => Algebra m (a, b) where
  algebra :: m (a, b) -> (a, b)
algebra m (a, b)
mab = (m a -> a
forall (m :: Type -> Type) a. Algebra m a => m a -> a
algebra (((a, b) -> a) -> m (a, b) -> m a
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a && b) ~> a
(a, b) -> a
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
forall a b. (Ob a, Ob b) => (a && b) ~> a
fst m (a, b)
mab), m b -> b
forall (m :: Type -> Type) a. Algebra m a => m a -> a
algebra (((a, b) -> b) -> m (a, b) -> m b
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a && b) ~> b
(a, b) -> b
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
forall a b. (Ob a, Ob b) => (a && b) ~> b
snd m (a, b)
mab))

type AlgebraicLens m s t a b = Optic (Strong (SUBCAT (Algebra m))) s t a b
mkAlgebraicLens :: forall m s t a b. (Monad m) => (s -> a) -> (m s -> b -> t) -> AlgebraicLens m s t a b
mkAlgebraicLens :: forall (m :: Type -> Type) s t a b.
Monad m =>
(s -> a) -> (m s -> b -> t) -> AlgebraicLens m s t a b
mkAlgebraicLens s -> a
v m s -> b -> t
u = forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d).
(CategoryOf c, CategoryOf d) =>
ExOptic m a b s t -> Optic (Strong m) s t a b
forall m a b s t.
(CategoryOf Type, CategoryOf Type) =>
ExOptic m a b s t -> Optic (Strong m) s t a b
ex2prof @(SUBCAT (Algebra m)) ((s ~> Act (SUB (m s)) a)
-> (SUB (m s) ~> SUB (m s))
-> (Act (SUB (m s)) b ~> t)
-> ExOptic (SUBCAT (Algebra m)) a b s t
forall {c} {d} {m} (b :: m) (t :: m) (a :: c) (b :: d) (s :: c)
       (t :: d).
(Ob a, Ob b) =>
(s ~> Act b a) -> (b ~> t) -> (Act t b ~> t) -> ExOptic m a b s t
ExOptic (\s
s -> (forall (m :: Type -> Type) a. Monad m => a -> m a
return @m s
s, s -> a
v s
s)) SUB (m s) ~> SUB (m s)
Sub (->) (SUB (m s)) (SUB (m s))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SUBCAT (Algebra m)). Ob a => Sub (->) a a
id ((m s -> b -> t) -> (m s, b) -> t
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry m s -> b -> t
u))

data Previewing a (b :: Type) s (t :: Type) where
  Previewing :: {forall s a b t. Previewing a b s t -> s -> Maybe a
unPreview :: s -> Maybe a} -> Previewing a b s t
instance Profunctor (Previewing a b) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> Previewing a b a b -> Previewing a b c d
dimap c ~> a
l b ~> d
_ (Previewing a -> Maybe a
f) = (c -> Maybe a) -> Previewing a b c d
forall s a b t. (s -> Maybe a) -> Previewing a b s t
Previewing (a -> Maybe a
f (a -> Maybe a) -> (c -> a) -> c -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
c -> a
l)
  (Ob a, Ob b) => r
r \\ :: forall a b r. ((Ob a, Ob b) => r) -> Previewing a b a b -> r
\\ Previewing a -> Maybe a
f = r
(Ob a, Ob b) => r
(Ob a, Ob (Maybe a)) => r
r ((Ob a, Ob (Maybe a)) => r) -> (a -> Maybe a) -> r
forall a b 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 -> Maybe a
f
instance Strong (COPROD Type) (Previewing a b) where
  act :: forall (a :: COPROD Type) (b :: COPROD Type) x y.
(a ~> b)
-> Previewing a b x y -> Previewing a b (Act a x) (Act b y)
act a ~> b
_ (Previewing x -> Maybe a
f) = (Either (UN 'COPR a) x -> Maybe a)
-> Previewing a b (Either (UN 'COPR a) x) (Either (UN 'COPR b) y)
forall s a b t. (s -> Maybe a) -> Previewing a b s t
Previewing ((UN 'COPR a -> Maybe a)
-> (x -> Maybe a) -> Either (UN 'COPR a) x -> Maybe a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe a -> UN 'COPR a -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing) x -> Maybe a
f)
instance Strong Type (Previewing a b) where
  act :: forall a b x y.
(a ~> b)
-> Previewing a b x y -> Previewing a b (Act a x) (Act b y)
act a ~> b
_ (Previewing x -> Maybe a
f) = ((a, x) -> Maybe a) -> Previewing a b (a, x) (b, y)
forall s a b t. (s -> Maybe a) -> Previewing a b s t
Previewing (x -> Maybe a
f (x -> Maybe a) -> ((a, x) -> x) -> (a, x) -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a && x) ~> x
(a, x) -> x
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
forall a b. (Ob a, Ob b) => (a && b) ~> b
snd)

infixl 8 ?.
(?.)
  :: s -> (Previewing a b a b -> Previewing a b s t) -> Maybe a
?. :: forall s a b t.
s -> (Previewing a b a b -> Previewing a b s t) -> Maybe a
(?.) s
s Previewing a b a b -> Previewing a b s t
l = Previewing a b s t -> s -> Maybe a
forall s a b t. Previewing a b s t -> s -> Maybe a
unPreview (Previewing a b a b -> Previewing a b s t
l (Previewing a b a b -> Previewing a b s t)
-> Previewing a b a b -> Previewing a b s t
forall a b. (a -> b) -> a -> b
$ (a -> Maybe a) -> Previewing a b a b
forall s a b t. (s -> Maybe a) -> Previewing a b s t
Previewing a -> Maybe a
forall a. a -> Maybe a
Just) s
s

type KlCat m = KLEISLI (Star (Prelude m))
data Updating a b s t where
  Update :: {forall {k} b s (m :: Type -> Type) t (a :: k).
Updating a ('KL b) s ('KL t) -> b -> s -> m t
unUpdate :: b -> s -> m t} -> Updating a (KL b :: KlCat m) s (KL t :: KlCat m)
instance (Monad m) => Profunctor (Updating a b :: KlCat m +-> Type) where
  dimap :: forall c a (b :: KlCat m) (d :: KlCat m).
(c ~> a) -> (b ~> d) -> Updating a b a b -> Updating a b c d
dimap c ~> a
l (Kleisli (Star a1 ~> Prelude m b1
r)) (Update b -> a -> m t
u) = (b -> c -> m b1) -> Updating a ('KL b) c ('KL b1)
forall {k} b s (m :: Type -> Type) t (a :: k).
(b -> s -> m t) -> Updating a ('KL b) s ('KL t)
Update (\b
b c
x -> b -> a -> m t
u b
b (c ~> a
c -> a
l c
x) m t -> (t -> m b1) -> m b1
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Prelude m b1 -> m b1
forall (f :: Type -> Type) a. Prelude f a -> f a
unPrelude (Prelude m b1 -> m b1) -> (a1 -> Prelude m b1) -> a1 -> m b1
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> Prelude m b1
a1 -> Prelude m b1
r)
  (Ob a, Ob b) => r
r \\ :: forall a (b :: KlCat m) r.
((Ob a, Ob b) => r) -> Updating a b a b -> r
\\ Update b -> a -> m t
u = r
(Ob a, Ob b) => r
(Ob b, Ob (a -> m t)) => r
r ((Ob b, Ob (a -> m t)) => r) -> (b -> a -> m t) -> r
forall a b 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 -> a -> m t
u
instance (Monad m) => Strong Type (Updating a b :: KlCat m +-> Type) where
  act :: forall a b x (y :: KlCat m).
(a ~> b) -> Updating a b x y -> Updating a b (Act a x) (Act b y)
act a ~> b
f (Update b -> x -> m t
u) = (b -> (a, x) -> m (b, t)) -> Updating a ('KL b) (a, x) ('KL (b, t))
forall {k} b s (m :: Type -> Type) t (a :: k).
(b -> s -> m t) -> Updating a ('KL b) s ('KL t)
Update (\b
b (a
a, x
x) -> (a ~> b
a -> b
f a
a,) (t -> (b, t)) -> m t -> m (b, t)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
`fmap` b -> x -> m t
u b
b x
x)

mupdate
  :: (Monad m)
  => (Updating a (KL b :: KlCat m) a (KL b :: KlCat m) -> Updating a (KL b :: KlCat m) s (KL t :: KlCat m))
  -> b
  -> s
  -> m t
mupdate :: forall (m :: Type -> Type) a b s t.
Monad m =>
(Updating a ('KL b) a ('KL b) -> Updating a ('KL b) s ('KL t))
-> b -> s -> m t
mupdate Updating a ('KL b) a ('KL b) -> Updating a ('KL b) s ('KL t)
f = Updating a ('KL b) s ('KL t) -> b -> s -> m t
forall {k} b s (m :: Type -> Type) t (a :: k).
Updating a ('KL b) s ('KL t) -> b -> s -> m t
unUpdate (Updating a ('KL b) s ('KL t) -> b -> s -> m t)
-> Updating a ('KL b) s ('KL t) -> b -> s -> m t
forall a b. (a -> b) -> a -> b
$ Updating a ('KL b) a ('KL b) -> Updating a ('KL b) s ('KL t)
f ((b -> a -> m b) -> Updating a ('KL b) a ('KL b)
forall {k} b s (m :: Type -> Type) t (a :: k).
(b -> s -> m t) -> Updating a ('KL b) s ('KL t)
Update (\b
b a
_ -> b -> m b
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return b
b))

newtype Replacing a b s t = Replace {forall a b s t. Replacing a b s t -> (a -> b) -> s -> t
unReplace :: (a -> b) -> (s -> t)}
instance Profunctor (Replacing a b) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> Replacing a b a b -> Replacing a b c d
dimap c ~> a
l b ~> d
r (Replace (a -> b) -> a -> b
f) = ((a -> b) -> c -> d) -> Replacing a b c d
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
ab -> b ~> d
b -> d
r (b -> d) -> (c -> b) -> c -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a -> b) -> a -> b
f a -> b
ab (a -> b) -> (c -> a) -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
c -> a
l)
instance Strong Type (Replacing a b) where
  act :: forall a b x y.
(a ~> b) -> Replacing a b x y -> Replacing a b (Act a x) (Act b y)
act a ~> b
w (Replace (a -> b) -> x -> y
f) = ((a -> b) -> (a, x) -> (b, y)) -> Replacing a b (a, x) (b, y)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
u -> (a -> b) -> (x -> y) -> (a, x) -> (b, y)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: Type +-> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a ~> b
a -> b
w ((a -> b) -> x -> y
f a -> b
u))
instance Strong (COPROD Type) (Replacing a b) where
  act :: forall (a :: COPROD Type) (b :: COPROD Type) x y.
(a ~> b) -> Replacing a b x y -> Replacing a b (Act a x) (Act b y)
act (Coprod (Id a1 ~> b1
w)) (Replace (a -> b) -> x -> y
f) = ((a -> b) -> Either a1 x -> Either b1 y)
-> Replacing a b (Either a1 x) (Either b1 y)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
u -> (a1 -> b1) -> (x -> y) -> Either a1 x -> Either b1 y
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: Type +-> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a1 ~> b1
a1 -> b1
w ((a -> b) -> x -> y
f a -> b
u))
instance Strong (Type -> Type) (Replacing a b) where
  act :: forall (a :: Type -> Type) (b :: Type -> Type) x y.
(a ~> b) -> Replacing a b x y -> Replacing a b (Act a x) (Act b y)
act a ~> b
w (Replace (a -> b) -> x -> y
f) = ((a -> b) -> a x -> b y) -> Replacing a b (a x) (b y)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
g -> a ~> b
Nat a b
w Nat a b -> (x ~> y) -> a x ~> b y
forall {j} {k} (f :: j -> k) (g :: j -> k) (a :: j) (b :: j).
Nat f g -> (a ~> b) -> f a ~> g b
! (a -> b) -> x -> y
f a -> b
g)

infixl 8 %~
(%~) :: (Replacing a b a b -> Replacing a b s t) -> (a -> b) -> (s -> t)
%~ :: forall a b s t.
(Replacing a b a b -> Replacing a b s t) -> (a -> b) -> s -> t
(%~) Replacing a b a b -> Replacing a b s t
l = Replacing a b s t -> (a -> b) -> s -> t
forall a b s t. Replacing a b s t -> (a -> b) -> s -> t
unReplace (Replacing a b a b -> Replacing a b s t
l (Replacing a b a b -> Replacing a b s t)
-> Replacing a b a b -> Replacing a b s t
forall a b. (a -> b) -> a -> b
$ ((a -> b) -> a -> b) -> Replacing a b a b
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (a -> b) -> a -> b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)

infixl 8 .~
(.~) :: (Replacing a b a b -> Replacing a b s t) -> b -> s -> t
Replacing a b a b -> Replacing a b s t
l .~ :: forall a b s t.
(Replacing a b a b -> Replacing a b s t) -> b -> s -> t
.~ b
b = Replacing a b a b -> Replacing a b s t
l (Replacing a b a b -> Replacing a b s t) -> (a -> b) -> s -> t
forall a b s t.
(Replacing a b a b -> Replacing a b s t) -> (a -> b) -> s -> t
%~ b -> a -> b
forall a b. a -> b -> a
const b
b

newtype Classifying m a b s t = Classifying
  {forall {k} (m :: Type -> Type) (a :: k) b s t.
Classifying m a b s t -> Monad m => m s -> b -> t
unClassify :: (Monad m) => m s -> b -> t}
instance (Monad m) => Profunctor (Classifying m a b) where
  dimap :: forall c a b d.
(c ~> a)
-> (b ~> d) -> Classifying m a b a b -> Classifying m a b c d
dimap c ~> a
l b ~> d
r (Classifying Monad m => m a -> b -> b
f) = (Monad m => m c -> b -> d) -> Classifying m a b c d
forall {k} (m :: Type -> Type) (a :: k) b s t.
(Monad m => m s -> b -> t) -> Classifying m a b s t
Classifying (\m c
u -> b ~> d
b -> d
r (b -> d) -> (b -> b) -> b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. m a -> b -> b
Monad m => m a -> b -> b
f ((c -> a) -> m c -> m a
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap c ~> a
c -> a
l m c
u))
instance (Monad m) => Strong (SUBCAT (Algebra m)) (Classifying m a b) where
  act :: forall (a :: SUBCAT (Algebra m)) (b :: SUBCAT (Algebra m)) x y.
(a ~> b)
-> Classifying m a b x y -> Classifying m a b (Act a x) (Act b y)
act (Sub a1 -> b1
w) (Classifying Monad m => m x -> b -> y
f) = (Monad m => m (a1, x) -> b -> (b1, y))
-> Classifying m a b (a1, x) (b1, y)
forall {k} (m :: Type -> Type) (a :: k) b s t.
(Monad m => m s -> b -> t) -> Classifying m a b s t
Classifying (\m (a1, x)
m b
b -> (m b1 -> b1
forall (m :: Type -> Type) a. Algebra m a => m a -> a
algebra (((a1, x) -> b1) -> m (a1, x) -> m b1
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a1 -> b1
w (a1 -> b1) -> ((a1, x) -> a1) -> (a1, x) -> b1
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a1 && x) ~> a1
(a1, x) -> a1
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
forall a b. (Ob a, Ob b) => (a && b) ~> a
fst) m (a1, x)
m), m x -> b -> y
Monad m => m x -> b -> y
f (((a1, x) -> x) -> m (a1, x) -> m x
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a1 && x) ~> x
(a1, x) -> x
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
forall a b. (Ob a, Ob b) => (a && b) ~> b
snd m (a1, x)
m) b
b))

infixl 8 .?
(.?) :: (Monad m) => (Classifying m a b a b -> Classifying m a b s t) -> b -> m s -> t
.? :: forall (m :: Type -> Type) a b s t.
Monad m =>
(Classifying m a b a b -> Classifying m a b s t) -> b -> m s -> t
(.?) Classifying m a b a b -> Classifying m a b s t
l b
b m s
ms = Classifying m a b s t -> Monad m => m s -> b -> t
forall {k} (m :: Type -> Type) (a :: k) b s t.
Classifying m a b s t -> Monad m => m s -> b -> t
unClassify (Classifying m a b a b -> Classifying m a b s t
l (Classifying m a b a b -> Classifying m a b s t)
-> Classifying m a b a b -> Classifying m a b s t
forall a b. (a -> b) -> a -> b
$ (Monad m => m a -> b -> b) -> Classifying m a b a b
forall {k} (m :: Type -> Type) (a :: k) b s t.
(Monad m => m s -> b -> t) -> Classifying m a b s t
Classifying ((b -> b) -> m a -> b -> b
forall a b. a -> b -> a
const b -> b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)) m s
ms b
b

instance InvertableOptic (Strong m) (Costrong m)
instance InvertableOptic (Costrong m) (Strong m)
instance (Strong m p) => Costrong m (Re p s t) where
  coact :: forall (a :: m) (x :: d) (y :: c).
(Ob a, Ob x, Ob y) =>
Re p s t (Act a x) (Act a y) -> Re p s t x y
coact @a (Re p (Act a y) (Act a x) -> p t s
f) = (p y x -> p t s) -> Re p s t x y
forall {k1} {k} (a :: k1) (b :: k) (p :: k -> k1 -> Type) (t :: k)
       (s :: k1).
(Ob a, Ob b) =>
(p b a -> p t s) -> Re p s t a b
Re \p y x
pyx -> p (Act a y) (Act a x) -> p t s
f ((a ~> a) -> p y x -> p (Act a y) (Act a x)
forall (a :: m) (b :: m) (x :: c) (y :: d).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) p y x
pyx)
instance (Costrong m p) => Strong m (Re p s t) where
  act :: forall (a :: m) (b :: m) (x :: d) (y :: c).
(a ~> b) -> Re p s t x y -> Re p s t (Act a x) (Act b y)
act @a @b @x @y a ~> b
g (Re p y x -> p t s
f) = a ~> b
g (a ~> b)
-> ((Ob a, Ob b) => Re p s t (Act a x) (Act b y))
-> Re p s t (Act a x) (Act b y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
    forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @m @_ @a @x ((Ob (Act a x) => Re p s t (Act a x) (Act b y))
 -> Re p s t (Act a x) (Act b y))
-> (Ob (Act a x) => Re p s t (Act a x) (Act b y))
-> Re p s t (Act a x) (Act b y)
forall a b. (a -> b) -> a -> b
$
      forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @m @_ @b @y ((Ob (Act b y) => Re p s t (Act a x) (Act b y))
 -> Re p s t (Act a x) (Act b y))
-> (Ob (Act b y) => Re p s t (Act a x) (Act b y))
-> Re p s t (Act a x) (Act b y)
forall a b. (a -> b) -> a -> b
$
        (p (Act b y) (Act a x) -> p t s) -> Re p s t (Act a x) (Act b y)
forall {k1} {k} (a :: k1) (b :: k) (p :: k -> k1 -> Type) (t :: k)
       (s :: k1).
(Ob a, Ob b) =>
(p b a -> p t s) -> Re p s t a b
Re \p (Act b y) (Act a x)
payax -> p y x -> p t s
f (forall {c} {d} m (p :: c +-> d) (a :: m) (x :: d) (y :: c).
(Costrong m p, Ob a, Ob x, Ob y) =>
p (Act a x) (Act a y) -> p x y
forall m (p :: d +-> c) (a :: m) (x :: c) (y :: d).
(Costrong m p, Ob a, Ob x, Ob y) =>
p (Act a x) (Act a y) -> p x y
coact @_ @_ @b ((Act a x ~> Act b x)
-> p (Act b y) (Act a x) -> p (Act b y) (Act b x)
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap ((a ~> b) -> (x ~> x) -> Act a x ~> Act b x
forall (a :: m) (b :: m) (x :: d) (y :: d).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a ~> b
g (forall (a :: d). (CategoryOf d, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x)) p (Act b y) (Act a x)
payax))

v1Optic :: Traversal (G.V1 a) (G.V1 a') a a'
v1Optic :: forall a a'. Traversal (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
copar0

u1Optic :: Traversal (G.U1 a) (G.U1 a') a a'
u1Optic :: forall a a'. Traversal (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
_ -> ()) (\() -> 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
par0

par1Optic :: Traversal (G.Par1 a) (G.Par1 a') a a'
par1Optic :: forall a a'. Traversal (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 :: Traversal (f a) (f a') a a' -> Traversal (G.Rec1 f a) (G.Rec1 f a') a a'
rec1Optic :: forall (f :: Type -> Type) a a'.
Traversal (f a) (f a') a a'
-> Traversal (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 :: Traversal (f a) (f a') a a' -> Traversal (G.M1 i k f a) (G.M1 i k f a') a a'
m1Optic :: forall (f :: Type -> Type) a a' i (k :: Meta).
Traversal (f a) (f a') a a'
-> Traversal (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'. Traversal (G.K1 i k a) (G.K1 i k a') a a'
k1Optic :: forall i k a a'. Traversal (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 :: CAT k} (a :: k).
(SelfAction k, Strong k p, MonoidalProfunctor p, Ob a) =>
p a a
strongPar0

plusOptic
  :: Traversal (p a) (p a') a a'
  -> Traversal (q a) (q a') a a'
  -> Traversal ((p G.:+: q) a) ((p G.:+: q) a') a a'
plusOptic :: forall (p :: Type -> Type) a a' (q :: Type -> Type).
Traversal (p a) (p a') a a'
-> Traversal (q a) (q a') a a'
-> Traversal ((:+:) 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)
`copar` 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
  :: Traversal (p a) (p a') a a'
  -> Traversal (q a) (q a') a a'
  -> Traversal ((p G.:*: q) a) ((p G.:*: q) a') a a'
multOptic :: forall (p :: Type -> Type) a a' (q :: Type -> Type).
Traversal (p a) (p a') a a'
-> Traversal (q a) (q a') a a'
-> Traversal ((:*:) 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'
f, q a'
g) -> p a'
f 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.:*: q a'
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)
`par` 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
  :: Traversal (p (q a)) (p (q a')) (q a) (q a')
  -> Traversal (q a) (q a') a a'
  -> Traversal ((p G.:.: q) a) ((p G.:.: q) a') a a'
compOptic :: forall (p :: Type -> Type) (q :: Type -> Type) a a'.
Traversal (p (q a)) (p (q a')) (q a) (q a')
-> Traversal (q a) (q a') a a'
-> Traversal ((:.:) 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))