{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Optics for an arbitrary 'Proarrow.Category.Monoidal.Action.MonoidalAction': the 'ActFl' flavor,
-- whose witness pair is a matched pair of arrows into\/out of the action at some residual; its
-- specialisation to the tensor's self-action gives 'MonoidalOptic'. Also home to the __algebraic
-- lens__ ('AlgLensFl'), the tensor-action pair with an 'Algebra'-for-a-monad residual, and its
-- list-monad case, the __classifying lens__ ('ClassifyFl'), which is moreover a kaleidoscope.
module Proarrow.Optic.Action where

import Data.Kind (Constraint)
import Prelude (($))
import Prelude qualified as P

import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , OplaxMonoidalRep
  , SymMonoidal
  , Tensor
  , obj2
  , swap
  , unpar0Rep
  , unparRep
  , type (**)
  )
import Proarrow.Category.Monoidal.Action (Act, ActionAt, MonoidalAction (..), composeActs, decomposeActs)
import Proarrow.Colimit.BinaryCoproduct (HasCoproducts)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (\\), type (+->))
import Proarrow.Functor (Functor)
import Proarrow.Monoid (Comonoid, Monoid)
import Proarrow.Monoid qualified as Mon
import Proarrow.Object (pattern Objs)
import Proarrow.Optic (ExOptic, FLAVOR, Optic, Prostrong (..), legs2prof, withLegs)
import Proarrow.Optic.Kaleidoscope (KaleidoFl)
import Proarrow.Optic.MonoidalLens (MonLensFl)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Star (Star)
import Proarrow.Profunctor.Representable (Rep (..), RepCostar (..), Representable (..))
import Proarrow.Promonad (Monad, bind, return)

-- | Any 'MonoidalAction' gives rise to a flavor: the witness pair is a matched pair of arrows
-- into\/out of the action for some shared, existentially hidden index @x@. 'Proarrow.Optic.Lens.LensFl'\/'Proarrow.Optic.Prism.PrismFl'
-- are (unspelled-out) special cases of this for 'Proarrow.Category.Monoidal.Action.ProdAction'\/'Proarrow.Category.Monoidal.Action.CoprodAction'.
type ActFl :: forall {m} {k}. (m, k) +-> k -> FLAVOR k k
class (MonoidalAction act, Profunctor p, Profunctor q) => ActFl act (p :: k +-> k) (q :: k +-> k) where
  withActP :: p s a -> q b t -> (forall x. (Ob x) => (s ~> Act act x a) -> (Act act x b ~> t) -> r) -> r

instance (MonoidalAction act, Ob x) => ActFl act (Rep (ActionAt act x)) (Corep (ActionAt act x)) where
  withActP :: forall (s :: j) (a :: j) (b :: j) (t :: j) r.
Rep (ActionAt act x) s a
-> Corep (ActionAt act x) b t
-> (forall (x :: m).
    Ob x =>
    (s ~> Act act x a) -> (Act act x b ~> t) -> r)
-> r
withActP (Rep s ~> (ActionAt act x @ a)
f) (Corep (ActionAt act x @ b) ~> t
g) forall (x :: m).
Ob x =>
(s ~> Act act x a) -> (Act act x b ~> t) -> r
k = forall (x :: m).
Ob x =>
(s ~> Act act x a) -> (Act act x b ~> t) -> r
k @x s ~> (ActionAt act x @ a)
s ~> Act act x a
f (ActionAt act x @ b) ~> t
Act act x b ~> t
g
instance (MonoidalAction act) => ActFl act (Id :: k +-> k) (Id :: k +-> k) where
  withActP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Id s a
-> Id b t
-> (forall (x :: m).
    Ob x =>
    (s ~> Act act x a) -> (Act act x b ~> t) -> r)
-> r
withActP (Id s ~> a
f) (Id b ~> t
g) forall (x :: m).
Ob x =>
(s ~> Act act x a) -> (Act act x b ~> t) -> r
k = forall (x :: m).
Ob x =>
(s ~> Act act x a) -> (Act act x b ~> t) -> r
k @Unit (forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
unitorInv @act (a ~> Act act Unit a) -> (s ~> a) -> s ~> Act act Unit a
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
f) (b ~> t
g (b ~> t) -> (Act act Unit b ~> b) -> Act act Unit b ~> 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 {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
unitor @act) ((Ob s, Ob a) => r) -> (s ~> a) -> 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
\\ s ~> a
f ((Ob b, Ob t) => r) -> (b ~> t) -> 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
\\ b ~> t
g
instance (ActFl act f g, ActFl act f' g') => ActFl act (f :.: f') (g' :.: g) where
  withActP :: forall (s :: i) (a :: i) (b :: i) (t :: i) r.
(:.:) f f' s a
-> (:.:) g' g b t
-> (forall (x :: m).
    Ob x =>
    (s ~> Act act x a) -> (Act act x b ~> t) -> r)
-> r
withActP @_ @a @b (f s b
f :.: f' :: f' b a
f'@f' b a
Objs) (g' :: g' b b
g'@g' b b
Objs :.: g b t
g) forall (x :: m).
Ob x =>
(s ~> Act act x a) -> (Act act x b ~> t) -> r
k =
    forall {m} {k} (act :: (m, k) +-> k) (p :: k +-> k) (q :: k +-> k)
       (s :: k) (a :: k) (b :: k) (t :: k) r.
ActFl act p q =>
p s a
-> q b t
-> (forall (x :: m).
    Ob x =>
    (s ~> Act act x a) -> (Act act x b ~> t) -> r)
-> r
forall (act :: (m, i) +-> i) (p :: i +-> i) (q :: i +-> i) (s :: i)
       (a :: i) (b :: i) (t :: i) r.
ActFl act p q =>
p s a
-> q b t
-> (forall (x :: m).
    Ob x =>
    (s ~> Act act x a) -> (Act act x b ~> t) -> r)
-> r
withActP @act @f @g f s b
f g b t
g \ @x s ~> Act act x b
f1 Act act x b ~> t
g1 ->
      forall {m} {k} (act :: (m, k) +-> k) (p :: k +-> k) (q :: k +-> k)
       (s :: k) (a :: k) (b :: k) (t :: k) r.
ActFl act p q =>
p s a
-> q b t
-> (forall (x :: m).
    Ob x =>
    (s ~> Act act x a) -> (Act act x b ~> t) -> r)
-> r
forall (act :: (m, i) +-> i) (p :: i +-> i) (q :: i +-> i) (s :: i)
       (a :: i) (b :: i) (t :: i) r.
ActFl act p q =>
p s a
-> q b t
-> (forall (x :: m).
    Ob x =>
    (s ~> Act act x a) -> (Act act x b ~> t) -> r)
-> r
withActP @act @f' @g' f' b a
f' g' b b
g' \ @y b ~> Act act x a
f2 Act act x b ~> b
g2 ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @y ((Ob (x ** x) => r) -> r) -> (Ob (x ** x) => r) -> r
forall a b. (a -> b) -> a -> b
$
          forall (x :: m).
Ob x =>
(s ~> Act act x a) -> (Act act x b ~> t) -> r
k @(x ** y) (forall {m} {k} (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k)
       (a :: k) (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(a ~> Act t x b) -> (b ~> Act t y c) -> a ~> Act t (x ** y) c
forall (t :: (m, i) +-> i) (x :: m) (y :: m) (c :: i) (a :: i)
       (b :: i).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(a ~> Act t x b) -> (b ~> Act t y c) -> a ~> Act t (x ** y) c
composeActs @act @x @y @a s ~> Act act x b
f1 b ~> Act act x a
f2) (forall {m} {k} (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k)
       (a :: k) (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(Act t y c ~> b) -> (Act t x b ~> a) -> Act t (x ** y) c ~> a
forall (t :: (m, i) +-> i) (x :: m) (y :: m) (c :: i) (a :: i)
       (b :: i).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(Act t y c ~> b) -> (Act t x b ~> a) -> Act t (x ** y) c ~> a
decomposeActs @act @x @y @b Act act x b ~> b
g2 Act act x b ~> t
g1)

type MonoidalOptic (s :: k) (t :: k) a b = Optic (Prostrong (ActFl Tensor)) 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 = forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR k k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @(ActFl Tensor) (forall (b :: k) (f :: k +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @a @(ActionAt Tensor m) s ~> (ActionAt Tensor m @ a)
s ~> (m ** a)
sma) (forall (a :: k) (f :: k +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep @b @(ActionAt Tensor m) (ActionAt Tensor m @ b) ~> t
(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)

-- | An Eilenberg-Moore algebra for the monad @m@ -- a representable 'Promonad' on @k@, acting as
-- the functor @m '%' -@ ("Proarrow.Promonad"): a structure map @m % a ~> a@, coherent with the
-- monad's unit and multiplication. The free algebras @m % s@ are the ones an algebraic lens is
-- built from ('algebraicLens').
--
-- There are deliberately no instances for the unit or for products of algebras, and there cannot be:
-- @Unit@ and @('**')@ are type families, which may not head an instance. That is why 'withAlgP'
-- passes the structure map as a /value/ -- the composition instance pairs two algebras with
-- 'unparRep' and the identity witness supplies the unit one with 'unpar0Rep', neither needing an
-- 'Algebra' instance. A witness pair whose residual is the unit is the identity optic up to the
-- unitors, so nothing is lost.
type Algebra :: forall {k}. (k +-> k) -> k -> Constraint
class (Monad m, Ob a) => Algebra (m :: k +-> k) (a :: k) where
  algebra :: m % a ~> a

-- | The free algebras of a monad @m@, wrapped as the representable promonad @'Star' m@.
instance (Monad (Star m), Ob (m a), Ob a) => Algebra (Star m) (m a) where
  algebra :: (Star m % m a) ~> m a
algebra = forall {j} (m :: j +-> j) (b :: j) (a :: j).
(Monad m, Ob b) =>
(a ~> (m % b)) -> (m % a) ~> (m % b)
forall (m :: k +-> k) (b :: k) (a :: k).
(Monad m, Ob b) =>
(a ~> (m % b)) -> (m % a) ~> (m % b)
bind @(Star m) m a ~> m a
m a ~> (Star m % a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

-- | The algebraic-lens flavor (Riley, /Categories of Optics/; Clarke et al.): the tensor-action
-- witness pair @'Rep'@\/@'Corep'@ @('ActionAt' 'Tensor' x)@ of "Proarrow.Optic.MonoidalLens" --
-- legs @s ~> x ** a@ and @x ** b ~> t@ -- with the residual @x@ an 'Algebra' for @m@. The flavor
-- itself asks only that the functor @m '%'@ be oplax monoidal, enough to pair and discard residuals;
-- the monad structure arrives with each 'Algebra' witness, not with the flavor.
-- The algebra is what lets @put@ see a whole @m@-computation of sources rather than one:
-- 'classifyOf' collapses @m % s@ to a single residual through it. Every algebraic lens is a
-- 'Proarrow.Optic.MonoidalLens.MonoidalLens' (the 'MonLensFl' superclass: the residual is a
-- comonoid), so it views, sets, folds and traverses as a lens does. 'withAlgP' hands the algebra
-- over as a value, so composites pair algebras without an instance for the product.
type AlgLensFl :: forall {k}. (k +-> k) -> FLAVOR k k
class (OplaxMonoidalRep m, MonLensFl p q) => AlgLensFl (m :: k +-> k) (p :: k +-> k) (q :: k +-> k) where
  -- | Recover the two legs and the algebra of the (existential) residual @x@.
  withAlgP
    :: p s a -> q b t -> (forall (x :: k). (Ob x) => (m % x ~> x) -> (s ~> x ** a) -> (x ** b ~> t) -> r) -> r

instance
  (OplaxMonoidalRep m, Algebra m x, Comonoid (x :: k))
  => AlgLensFl m (Rep (ActionAt Tensor x) :: k +-> k) (Corep (ActionAt Tensor x))
  where
  withAlgP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Rep (ActionAt Tensor x) s a
-> Corep (ActionAt Tensor x) b t
-> (forall (x :: k).
    Ob x =>
    ((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r)
-> r
withAlgP (Rep s ~> (ActionAt Tensor x @ a)
h) (Corep (ActionAt Tensor x @ b) ~> t
i) forall (x :: k).
Ob x =>
((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r
k = forall (x :: k).
Ob x =>
((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r
k @x (forall {k} (m :: k +-> k) (a :: k). Algebra m a => (m % a) ~> a
forall (m :: k +-> k) (a :: k). Algebra m a => (m % a) ~> a
algebra @m @x) s ~> (ActionAt Tensor x @ a)
s ~> (x ** a)
h (ActionAt Tensor x @ b) ~> t
(x ** b) ~> t
i
instance (OplaxMonoidalRep (m :: k +-> k)) => AlgLensFl m (Id :: k +-> k) (Id :: k +-> k) where
  withAlgP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Id s a
-> Id b t
-> (forall (x :: k).
    Ob x =>
    ((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r)
-> r
withAlgP (Id s ~> a
l) (Id b ~> t
r) forall (x :: k).
Ob x =>
((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r
k = forall (x :: k).
Ob x =>
((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r
k @Unit (forall {j} {k} (p :: j +-> k).
OplaxMonoidalRep p =>
(p % Unit) ~> Unit
forall (p :: k +-> k). OplaxMonoidalRep p => (p % Unit) ~> Unit
unpar0Rep @m) (a ~> (Unit ** a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv (a ~> (Unit ** a)) -> (s ~> a) -> s ~> (Unit ** a)
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
l) (b ~> t
r (b ~> t) -> ((Unit ** b) ~> b) -> (Unit ** b) ~> 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
. (Unit ** b) ~> b
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor) ((Ob s, Ob a) => r) -> (s ~> a) -> 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
\\ s ~> a
l ((Ob b, Ob t) => r) -> (b ~> t) -> 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
\\ b ~> t
r
instance
  forall k (m :: k +-> k) (f :: k +-> k) (f' :: k +-> k) (g :: k +-> k) (g' :: k +-> k)
   . (AlgLensFl m f g, AlgLensFl m f' g')
  => AlgLensFl m (f :.: f') (g' :.: g)
  where
  withAlgP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
(:.:) f f' s a
-> (:.:) g' g b t
-> (forall (x :: k).
    Ob x =>
    ((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r)
-> r
withAlgP @_ @afoc @bfoc (f s b
f :.: f' :: f' b a
f'@f' b a
Objs) (g' :: g' b b
g'@g' b b
Objs :.: g b t
g) forall (x :: k).
Ob x =>
((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r
kk =
    forall {k} (m :: k +-> k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k) r.
AlgLensFl m p q =>
p s a
-> q b t
-> (forall (x :: k).
    Ob x =>
    ((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r)
-> r
forall (m :: k +-> k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k) r.
AlgLensFl m p q =>
p s a
-> q b t
-> (forall (x :: k).
    Ob x =>
    ((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r)
-> r
withAlgP @m f s b
f g b t
g \ @(xo :: k) (m % x) ~> x
algo s ~> (x ** b)
ho (x ** b) ~> t
io ->
      forall {k} (m :: k +-> k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k) r.
AlgLensFl m p q =>
p s a
-> q b t
-> (forall (x :: k).
    Ob x =>
    ((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r)
-> r
forall (m :: k +-> k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k) r.
AlgLensFl m p q =>
p s a
-> q b t
-> (forall (x :: k).
    Ob x =>
    ((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r)
-> r
withAlgP @m f' b a
f' g' b b
g' \ @(xi :: k) (m % x) ~> x
algi b ~> (x ** a)
hi (x ** b) ~> b
ii ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @xo @xi
          ( forall (x :: k).
Ob x =>
((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r
kk @(xo ** xi)
              (((m % x) ~> x
algo ((m % x) ~> x)
-> ((m % x) ~> x) -> ((m % x) ** (m % x)) ~> (x ** x)
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)
** (m % x) ~> x
algi) (((m % x) ** (m % x)) ~> (x ** x))
-> ((m % (x ** x)) ~> ((m % x) ** (m % x)))
-> (m % (x ** x)) ~> (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 {j} {k} (p :: j +-> k) (x :: j) (y :: j).
(OplaxMonoidalRep p, Ob x, Ob y) =>
(p % (x ** y)) ~> ((p % x) ** (p % y))
forall (p :: k +-> k) (x :: k) (y :: k).
(OplaxMonoidalRep p, Ob x, Ob y) =>
(p % (x ** y)) ~> ((p % x) ** (p % y))
unparRep @m @xo @xi)
              (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @xo @xi @afoc ((x ** (x ** a)) ~> ((x ** x) ** a))
-> (s ~> (x ** (x ** a))) -> s ~> ((x ** x) ** a)
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 @xo Obj x -> (b ~> (x ** a)) -> (x ** b) ~> (x ** (x ** 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)
** b ~> (x ** a)
hi) ((x ** b) ~> (x ** (x ** a)))
-> (s ~> (x ** b)) -> s ~> (x ** (x ** a))
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 ~> (x ** b)
ho)
              ((x ** b) ~> t
io ((x ** b) ~> t)
-> (((x ** x) ** b) ~> (x ** b)) -> ((x ** x) ** b) ~> 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 @xo Obj x -> ((x ** b) ~> b) -> (x ** (x ** b)) ~> (x ** 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)
** (x ** b) ~> b
ii) ((x ** (x ** b)) ~> (x ** b))
-> (((x ** x) ** b) ~> (x ** (x ** b)))
-> ((x ** x) ** b) ~> (x ** 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 k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @xo @xi @bfoc)
          )

-- | An algebraic lens: like a 'Proarrow.Optic.Lens.Lens', but @put@ is allowed to combine
-- information monadically -- @get :: s ~> a@, @put :: m % s ** b ~> t@ -- rather than only ever
-- seeing the /last/ @s@.
type AlgebraicLens m (s :: k) (t :: k) a b = Optic (Prostrong (AlgLensFl m)) s t a b

-- | Build an algebraic lens from @get@ and a monadic @put@; the residual is the free algebra
-- @m % s@ itself (which must be a comonoid, as must @s@ to be kept alongside its focus).
algebraicLens
  :: forall {k} m (s :: k) (t :: k) a b
   . (Algebra m (m % s), Comonoid (m % s), Comonoid s, OplaxMonoidalRep m, Ob a, Ob b)
  => (s ~> a) -> (m % s ** b ~> t) -> AlgebraicLens m s t a b
algebraicLens :: forall {k} (m :: k +-> k) (s :: k) (t :: k) (a :: k) (b :: k).
(Algebra m (m % s), Comonoid (m % s), Comonoid s,
 OplaxMonoidalRep m, Ob a, Ob b) =>
(s ~> a) -> (((m % s) ** b) ~> t) -> AlgebraicLens m s t a b
algebraicLens s ~> a
v ((m % s) ** b) ~> t
u =
  forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR k k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @(AlgLensFl m)
    (forall (b :: k) (f :: k +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @a @(ActionAt Tensor (m % s)) ((forall {j} (m :: j +-> j) (a :: j). (Monad m, Ob a) => a ~> (m % a)
forall (m :: k +-> k) (a :: k). (Monad m, Ob a) => a ~> (m % a)
return @m @s (s ~> (m % s)) -> (s ~> a) -> (s ** s) ~> ((m % s) ** 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)
** s ~> a
v) ((s ** s) ~> ((m % s) ** a))
-> (s ~> (s ** s)) -> s ~> ((m % s) ** a)
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 (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
Mon.comult @s))
    (forall (a :: k) (f :: k +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep @b @(ActionAt Tensor (m % s)) (ActionAt Tensor (m % s) @ b) ~> t
((m % s) ** b) ~> t
u)

-- | Classify a monadic computation of @s@'s through an 'AlgebraicLens' (or any stronger optic,
-- in any encoding), given a replacement focus @b@ -- generalizing "set" to combine every @s@ the
-- computation might produce (via its residual's 'Algebra') rather than only ever seeing the last one.
-- The focus @a@ is discarded under the monad, hence must be a comonoid.
classifyOf
  :: forall {k} m c (s :: k) (t :: k) a b
   . (OplaxMonoidalRep m, Comonoid a, (Ob a, Ob b) => c (ExOptic (AlgLensFl m) a b))
  => Optic c s t a b -> (m % s ** b) ~> t
classifyOf :: forall {k} (m :: k +-> k) (c :: (k +-> k) -> Constraint) (s :: k)
       (t :: k) (a :: k) (b :: k).
(OplaxMonoidalRep m, Comonoid a,
 (Ob a, Ob b) => c (ExOptic (AlgLensFl m) a b)) =>
Optic c s t a b -> ((m % s) ** b) ~> t
classifyOf Optic c s t a b
optic =
  forall {j} {k} (w :: FLAVOR j k)
       (c :: (k -> j -> Type) -> Constraint) (s :: k) (t :: j) (a :: k)
       (b :: j) r.
(CategoryOf j, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: j +-> j).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
forall (w :: FLAVOR k k) (c :: (k +-> k) -> Constraint) (s :: k)
       (t :: k) (a :: k) (b :: k) r.
(CategoryOf k, CategoryOf k, Flavor w,
 (Ob a, Ob b) => c (ExOptic w a b)) =>
Optic c s t a b
-> (forall (p :: k +-> k) (q :: k +-> k).
    (w p q, Profunctor p, Profunctor q) =>
    p s a -> q b t -> r)
-> r
withLegs @(AlgLensFl m) Optic c s t a b
optic \p s a
l q b t
r ->
    forall {k} (m :: k +-> k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k) r.
AlgLensFl m p q =>
p s a
-> q b t
-> (forall (x :: k).
    Ob x =>
    ((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r)
-> r
forall (m :: k +-> k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k) r.
AlgLensFl m p q =>
p s a
-> q b t
-> (forall (x :: k).
    Ob x =>
    ((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r)
-> r
withAlgP @m p s a
l q b t
r \ @x (m % x) ~> x
alg s ~> (x ** a)
h (x ** b) ~> t
i ->
      ((x ** b) ~> t
i ((x ** b) ~> t)
-> (((m % s) ** b) ~> (x ** b)) -> ((m % s) ** b) ~> 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
. (((m % x) ~> x
alg ((m % x) ~> x) -> ((m % s) ~> (m % x)) -> (m % s) ~> 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 {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @m (forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @x ((x ** Unit) ~> x) -> (s ~> (x ** Unit)) -> s ~> 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). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x Obj x -> (a ~> Unit) -> (x ** a) ~> (x ** Unit)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
Mon.counit @a) ((x ** a) ~> (x ** Unit)) -> (s ~> (x ** a)) -> s ~> (x ** Unit)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (x ** a)
h)) ((m % s) ~> x) -> (b ~> b) -> ((m % s) ** b) ~> (x ** 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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)) ((Ob b, Ob t) => ((m % s) ** b) ~> t)
-> q b t -> ((m % s) ** b) ~> t
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> q 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
\\ q b t
r

infixl 8 .?

-- | 'classifyOf' for a Haskell monad, curried: @optic .? b $ fs@.
(.?)
  :: forall f c s t a b
   . (P.Monad f, Functor f, c (ExOptic (AlgLensFl (Star f)) a b))
  => Optic c s t a b -> b -> f s -> t
.? :: forall (f :: Type -> Type)
       (c :: (Type -> Type -> Type) -> Constraint) s t a b.
(Monad f, Functor f, c (ExOptic (AlgLensFl (Star f)) a b)) =>
Optic c s t a b -> b -> f s -> t
(.?) Optic c s t a b
l b
b f s
fs = forall {k} (m :: k +-> k) (c :: (k +-> k) -> Constraint) (s :: k)
       (t :: k) (a :: k) (b :: k).
(OplaxMonoidalRep m, Comonoid a,
 (Ob a, Ob b) => c (ExOptic (AlgLensFl m) a b)) =>
Optic c s t a b -> ((m % s) ** b) ~> t
forall (m :: Type -> Type -> Type)
       (c :: (Type -> Type -> Type) -> Constraint) s t a b.
(OplaxMonoidalRep m, Comonoid a,
 (Ob a, Ob b) => c (ExOptic (AlgLensFl m) a b)) =>
Optic c s t a b -> ((m % s) ** b) ~> t
classifyOf @(Star f) Optic c s t a b
l (f s
fs, b
b)

-- | The __classifying lens__ (Clarke et al., Example 3.11): the algebraic lens for the list monad,
-- here for any monad @l@ whose algebras are monoids. Tensoring with a monoid is an applicative
-- functor (the writer applicative) -- so a classifying lens is also a kaleidoscope
-- ('Proarrow.Optic.Kaleidoscope.KaleidoFl'), the meet of the two flavors. This is what lets it compose
-- with a kaleidoscope to a kaleidoscope again (Clarke et al., Remark 3.28): a lens composed
-- with a kaleidoscope is not a kaleidoscope, since a product functor is not applicative, but a
-- product /by a monoid/ is. The algebra and the monoid on the residual are assumed to agree, as
-- they do for the free algebra @l % s@ of the list monad (@join@ and @++@) that 'classifyingLens' uses.
type ClassifyFl :: forall {k}. (k +-> k) -> FLAVOR k k
class (AlgLensFl l p q, KaleidoFl p q) => ClassifyFl (l :: k +-> k) (p :: k +-> k) (q :: k +-> k)

instance
  (OplaxMonoidalRep l, Algebra l x, Monoid x, Comonoid x, SymMonoidal k, HasCoproducts k)
  => ClassifyFl l (Rep (ActionAt Tensor x) :: k +-> k) (Corep (ActionAt Tensor x))
instance (OplaxMonoidalRep (l :: k +-> k)) => ClassifyFl l (Id :: k +-> k) (Id :: k +-> k)
instance (ClassifyFl l f g, ClassifyFl l f' g') => ClassifyFl l (f :.: f') (g' :.: g)

type ClassifyingLens l (s :: k) (t :: k) a b = Optic (Prostrong (ClassifyFl l)) s t a b

-- | Build a classifying lens from @get@ and a @classify :: l % s ** b ~> t@; the residual is the
-- free algebra @l % s@, e.g. the list of sources.
classifyingLens
  :: forall {k} l (s :: k) (t :: k) a b
   . ( Algebra l (l % s)
     , Monoid (l % s)
     , Comonoid (l % s)
     , Comonoid s
     , OplaxMonoidalRep l
     , SymMonoidal k
     , HasCoproducts k
     , Ob a
     , Ob b
     )
  => (s ~> a) -> (l % s ** b ~> t) -> ClassifyingLens l s t a b
classifyingLens :: forall {k} (l :: k +-> k) (s :: k) (t :: k) (a :: k) (b :: k).
(Algebra l (l % s), Monoid (l % s), Comonoid (l % s), Comonoid s,
 OplaxMonoidalRep l, SymMonoidal k, HasCoproducts k, Ob a, Ob b) =>
(s ~> a) -> (((l % s) ** b) ~> t) -> ClassifyingLens l s t a b
classifyingLens s ~> a
v ((l % s) ** b) ~> t
u =
  forall {j} {k} (w :: FLAVOR j k) (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
forall (w :: FLAVOR k k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (t :: k) (a :: k) (b :: k).
(CategoryOf k, CategoryOf k, w p q, Profunctor p, Profunctor q) =>
p s a -> q b t -> Optic (Prostrong w) s t a b
legs2prof @(ClassifyFl l)
    (forall (b :: k) (f :: k +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep @a @(ActionAt Tensor (l % s)) ((forall {j} (m :: j +-> j) (a :: j). (Monad m, Ob a) => a ~> (m % a)
forall (m :: k +-> k) (a :: k). (Monad m, Ob a) => a ~> (m % a)
return @l @s (s ~> (l % s)) -> (s ~> a) -> (s ** s) ~> ((l % s) ** 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)
** s ~> a
v) ((s ** s) ~> ((l % s) ** a))
-> (s ~> (s ** s)) -> s ~> ((l % s) ** a)
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 (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
Mon.comult @s))
    (forall (a :: k) (f :: k +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep @b @(ActionAt Tensor (l % s)) (ActionAt Tensor (l % s) @ b) ~> t
((l % s) ** b) ~> t
u)

-- | The carrier of the literature's algebraic-lens eliminator: @'RepCostar' m@, i.e. @m % a ~> b@.
-- Absorbing an algebraic-lens witness pair collapses the residuals of the incoming computation
-- through their algebra and hands the foci on as one @m@-computation.
instance (OplaxMonoidalRep (m :: k +-> k)) => Prostrong (AlgLensFl m) (RepCostar m :: k +-> k) where
  proact :: forall (f :: k +-> k) (g :: k +-> k).
(AlgLensFl m f g, Profunctor f, Profunctor g) =>
((f :.: RepCostar m) :.: g) :~> RepCostar m
proact (f a b
f :.: RepCostar @afoc (m % b) ~> b
g :.: g b b
g') =
    forall {k} (m :: k +-> k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k) r.
AlgLensFl m p q =>
p s a
-> q b t
-> (forall (x :: k).
    Ob x =>
    ((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r)
-> r
forall (m :: k +-> k) (p :: k +-> k) (q :: k +-> k) (s :: k)
       (a :: k) (b :: k) (t :: k) r.
AlgLensFl m p q =>
p s a
-> q b t
-> (forall (x :: k).
    Ob x =>
    ((m % x) ~> x) -> (s ~> (x ** a)) -> ((x ** b) ~> t) -> r)
-> r
withAlgP @m f a b
f g b b
g' \ @x (m % x) ~> x
alg a ~> (x ** b)
h (x ** b) ~> b
i ->
      ((m % a) ~> b) -> RepCostar m a b
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar ((x ** b) ~> b
i ((x ** b) ~> b) -> ((m % a) ~> (x ** b)) -> (m % 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
. ((m % x) ~> x
alg ((m % x) ~> x)
-> ((m % b) ~> b) -> ((m % x) ** (m % b)) ~> (x ** 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)
** (m % b) ~> b
g) (((m % x) ** (m % b)) ~> (x ** b))
-> ((m % a) ~> ((m % x) ** (m % b))) -> (m % a) ~> (x ** 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 {j} {k} (p :: j +-> k) (x :: j) (y :: j).
(OplaxMonoidalRep p, Ob x, Ob y) =>
(p % (x ** y)) ~> ((p % x) ** (p % y))
forall (p :: k +-> k) (x :: k) (y :: k).
(OplaxMonoidalRep p, Ob x, Ob y) =>
(p % (x ** y)) ~> ((p % x) ** (p % y))
unparRep @m @x @afoc ((m % (x ** b)) ~> ((m % x) ** (m % b)))
-> ((m % a) ~> (m % (x ** b))) -> (m % a) ~> ((m % x) ** (m % 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 {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @m a ~> (x ** b)
h) ((Ob (m % b), Ob b) => RepCostar m a b)
-> ((m % b) ~> b) -> RepCostar m 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
\\ (m % b) ~> b
g ((Ob a, Ob b) => RepCostar m a b) -> f a b -> RepCostar m a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> f 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
\\ f a b
f