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

-- | The __monoidal lens__: the coend optic for the tensor action with a __comonoidal residual__,
--
-- > MonoidalLens s t a b = exists m. Comonoid m => (s ~> m ** a, m ** b ~> t)
--
-- The residual can be discarded (@'counit' :: m ~> 'Unit'@) and copied, which is what a lens's
-- @get@ needs, so a monoidal lens views, sets, folds and traverses:
--
-- > Lens         <: { Getter, AffineTraversal, Glass }                     -- product residual
-- > MonoidalLens <: { Getter, MonoidalTraversal, AffineTraversal, Glass }  -- comonoidal tensor residual
--
-- It is not a 'Proarrow.Optic.Lens.Lens', because 'Proarrow.Optic.Lens.putP' works with binary
-- products alone, unrelated to the tensor. It is an
-- 'Proarrow.Optic.AffineTraversal.AffineTraversal' and a 'Proarrow.Optic.Glass.Glass', because
-- their methods ask for a cartesian category, where the tensor is the product and the residual can
-- be projected out.
module Proarrow.Optic.MonoidalLens where

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal, Tensor)
import Proarrow.Category.Monoidal.Action (ActionAt)
import Proarrow.Colimit.BinaryCoproduct (lft, rgt)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (\\), type (+->))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), first)
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (Comonoid, ComonoidOn, comonoidOn, tensorComonoid, unitComonoid)
import Proarrow.Monoid qualified as Mon
import Proarrow.Object (pattern Objs)
import Proarrow.Optic
  ( ExOptic
  , FLAVOR
  , Optic
  , Prostrong (..)
  , legs2prof
  , withLegs
  )
import Proarrow.Optic.AffineFold (AffineFoldFl (..))
import Proarrow.Optic.AffineTraversal (AffineTravFl (..))
import Proarrow.Optic.Getter (GetterFl (..))
import Proarrow.Optic.Glass (GlassFl (..), Mod, applySel, withObSel)
import Proarrow.Optic.Traversal (MonTravFl)
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..))
import Prelude (($))

-- | The tensor-action witness pair @'Rep'@\/@'Corep'@ @('ActionAt' 'Tensor' m)@ views (and previews)
-- when the residual @m@ is a 'Comonoid': discard it with the counit. (Its setter and traversal
-- instances live in "Proarrow.Optic.Setter" and "Proarrow.Optic.Traversal".)
instance (Comonoid (m :: k)) => AffineFoldFl (Rep (ActionAt Tensor m) :: k +-> k) (Corep (ActionAt Tensor m)) where
  previewP :: forall (s :: k) (a :: k).
Bicartesian k =>
Rep (ActionAt Tensor m) s a -> s ~> (a || TerminalObject)
previewP @_ @a (Rep s ~> (ActionAt Tensor m @ a)
h) = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @TerminalObject (a ~> (a || TerminalObject))
-> (s ~> a) -> s ~> (a || TerminalObject)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Unit ** a) ~> a
(TerminalObject ** a) ~> a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((TerminalObject ** a) ~> a)
-> (s ~> (TerminalObject ** a)) -> s ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
Mon.counit @m (m ~> TerminalObject)
-> (a ~> a) -> (m ** a) ~> (TerminalObject ** 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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) ((m ** a) ~> (TerminalObject ** a))
-> (s ~> (m ** a)) -> s ~> (TerminalObject ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (ActionAt Tensor m @ a)
s ~> (m ** a)
h

instance (Comonoid (m :: k)) => GetterFl (Rep (ActionAt Tensor m) :: k +-> k) (Corep (ActionAt Tensor m)) where
  getP :: forall (s :: k) (a :: k). Rep (ActionAt Tensor m) s a -> s ~> a
getP @_ @a (Rep s ~> (ActionAt Tensor m @ a)
h) = (Unit ** a) ~> a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((Unit ** a) ~> a) -> (s ~> (Unit ** a)) -> s ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
Mon.counit @m (m ~> Unit) -> (a ~> a) -> (m ** a) ~> (Unit ** 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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) ((m ** a) ~> (Unit ** a)) -> (s ~> (m ** a)) -> s ~> (Unit ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (ActionAt Tensor m @ a)
s ~> (m ** a)
h

-- | In a cartesian category the tensor /is/ the product, so the comonoidal residual can be
-- projected out and put back: 'affineSet' and 'glassP' carry that assumption in their own
-- constraints ('Bicartesian', 'CCC'), which is why these instances exist while a 'LensFl' one
-- cannot ('putP' has only 'HasBinaryProducts').
instance (Comonoid (m :: k)) => AffineTravFl (Rep (ActionAt Tensor m) :: k +-> k) (Corep (ActionAt Tensor m)) where
  -- a lens always matches
  affineMatch :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Bicartesian k =>
Rep (ActionAt Tensor m) s a
-> Corep (ActionAt Tensor m) b t -> s ~> (t || a)
affineMatch @_ @a @_ @t (Rep s ~> (ActionAt Tensor m @ a)
h) Corep (ActionAt Tensor m) b t
Objs = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @t @a (a ~> (t || a)) -> (s ~> a) -> s ~> (t || a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Unit ** a) ~> a
(TerminalObject ** a) ~> a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((TerminalObject ** a) ~> a)
-> (s ~> (TerminalObject ** a)) -> s ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
Mon.counit @m (m ~> TerminalObject)
-> (a ~> a) -> (m ** a) ~> (TerminalObject ** 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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) ((m ** a) ~> (TerminalObject ** a))
-> (s ~> (m ** a)) -> s ~> (TerminalObject ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (ActionAt Tensor m @ a)
s ~> (m ** a)
h
  affineSet :: forall (s :: k) (a :: k) (b :: k) (t :: k).
Bicartesian k =>
Rep (ActionAt Tensor m) s a
-> Corep (ActionAt Tensor m) b t -> (s && b) ~> t
affineSet @_ @a @b (Rep s ~> (ActionAt Tensor m @ a)
h) (Corep (ActionAt Tensor m @ b) ~> t
i) = (ActionAt Tensor m @ b) ~> t
(m ** b) ~> t
i ((m ** b) ~> t) -> ((s && b) ~> (m ** b)) -> (s && b) ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
forall {k} (c :: k) (a :: k) (b :: k).
(HasBinaryProducts k, Ob c) =>
(a ~> b) -> (a && c) ~> (b && c)
first @b (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @m @a ((m && a) ~> m) -> (s ~> (m && a)) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (ActionAt Tensor m @ a)
s ~> (m && a)
h)

instance (Comonoid (m :: k)) => GlassFl (Rep (ActionAt Tensor m) :: k +-> k) (Corep (ActionAt Tensor m)) where
  glassP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
CCC k =>
Rep (ActionAt Tensor m) s a
-> Corep (ActionAt Tensor m) b t -> (s && Mod s a b) ~> t
glassP @s @a @b (Rep h :: s ~> (ActionAt Tensor m @ a)
h@s ~> (ActionAt Tensor m @ a)
s ~> (m ** a)
Objs) (Corep (ActionAt Tensor m @ b) ~> t
i) =
    forall (s :: k) (a :: k) (b :: k) r.
(Closed k, Ob s, Ob a, Ob b) =>
((Ob (s ~~> a), Ob (Mod s a b)) => r) -> r
forall {k} (s :: k) (a :: k) (b :: k) r.
(Closed k, Ob s, Ob a, Ob b) =>
((Ob (s ~~> a), Ob (Mod s a b)) => r) -> r
withObSel @s @a @b (((Ob (s ~~> a), Ob (Mod s a b)) => (s && Mod s a b) ~> t)
 -> (s && Mod s a b) ~> t)
-> ((Ob (s ~~> a), Ob (Mod s a b)) => (s && Mod s a b) ~> t)
-> (s && Mod s a b) ~> t
forall a b. (a -> b) -> a -> b
$
      (ActionAt Tensor m @ b) ~> t
(m ** b) ~> t
i
        ((m ** b) ~> t)
-> ((s && Mod s a b) ~> (m ** b)) -> (s && Mod s a b) ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ( (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @m @a ((m && a) ~> m)
-> ((s && Mod s a b) ~> (m && a)) -> (s && Mod s a b) ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (ActionAt Tensor m @ a)
s ~> (m && a)
h (s ~> (m && a))
-> ((s && Mod s a b) ~> s) -> (s && Mod s a b) ~> (m && a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @s @(Mod s a b))
              ((s && Mod s a b) ~> m)
-> ((s && Mod s a b) ~> b) -> (s && Mod s a b) ~> (m && b)
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)
&&& (forall (s :: k) (a :: k) (b :: k).
(Closed k, Ob s, Ob a, Ob b) =>
(s ~> a) -> Mod s a b ~> b
forall {k} (s :: k) (a :: k) (b :: k).
(Closed k, Ob s, Ob a, Ob b) =>
(s ~> a) -> Mod s a b ~> b
applySel @s @a @b (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @m @a ((m && a) ~> a) -> (s ~> (m && a)) -> s ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (ActionAt Tensor m @ a)
s ~> (m && a)
h) (Mod s a b ~> b)
-> ((s && Mod s a b) ~> Mod s a b) -> (s && Mod s a b) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @s @(Mod s a b))
          )

-- | The monoidal-lens flavor: a lens whose residual is a comonoid, so it is a
-- 'Proarrow.Optic.Getter.Getter' and a 'Proarrow.Optic.MonoidalTraversal.MonoidalTraversal', and
-- in cartesian categories an 'Proarrow.Optic.AffineTraversal.AffineTraversal' and a
-- 'Proarrow.Optic.Glass.Glass'.
type MonLensFl :: forall {k}. FLAVOR k k
class (GetterFl p q, MonTravFl p q, AffineTravFl p q, GlassFl p q) => MonLensFl (p :: k +-> k) (q :: k +-> k) where
  -- | Recover a monoidal lens's two legs and the comonoid structure of its existential residual
  -- @m@. The comonoid comes as a value ('ComonoidOn') rather than a 'Comonoid' constraint, because
  -- the residual of a composite is a tensor and that of the identity the unit, and type families
  -- cannot head an instance. A tensor of comonoids is a comonoid by symmetry.
  withMonLensP
    :: (SymMonoidal k)
    => p s a -> q b t -> (forall (m :: k). (Ob m) => ComonoidOn m -> (s ~> m ** a) -> (m ** b ~> t) -> r) -> r

instance (Comonoid (m :: k)) => MonLensFl (Rep (ActionAt Tensor m) :: k +-> k) (Corep (ActionAt Tensor m)) where
  withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
SymMonoidal k =>
Rep (ActionAt Tensor m) s a
-> Corep (ActionAt Tensor m) b t
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP (Rep s ~> (ActionAt Tensor m @ a)
h) (Corep (ActionAt Tensor m @ b) ~> t
i) forall (m :: k).
Ob m =>
ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k = forall (m :: k).
Ob m =>
ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k @m (forall (c :: k). Comonoid c => ComonoidOn c
forall {k} (c :: k). Comonoid c => ComonoidOn c
comonoidOn @m) s ~> (ActionAt Tensor m @ a)
s ~> (m ** a)
h (ActionAt Tensor m @ b) ~> t
(m ** b) ~> t
i

instance (CategoryOf k) => MonLensFl (Id :: k +-> k) (Id :: k +-> k) where
  withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
SymMonoidal k =>
Id s a
-> Id b t
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP (Id s ~> a
sa) (Id b ~> t
bt) forall (m :: k).
Ob m =>
ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k = forall (m :: k).
Ob m =>
ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k @Unit ComonoidOn Unit
forall {k}. Monoidal k => ComonoidOn Unit
unitComonoid (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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> a
sa) (b ~> t
bt (b ~> t) -> ((Unit ** b) ~> b) -> (Unit ** b) ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (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
sa ((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
bt

instance
  forall k (f :: k +-> k) (f' :: k +-> k) (g :: k +-> k) (g' :: k +-> k)
   . (MonLensFl f g, MonLensFl f' g')
  => MonLensFl (f :.: f') (g' :.: g)
  where
  withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
SymMonoidal k =>
(:.:) f f' s a
-> (:.:) g' g b t
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP (f s b
f :.: (f' :: f' b a
f'@f' b a
Objs :: f' hix afoc)) ((g' :: g' b b
g'@g' b b
Objs :: g' bfoc giy) :.: g b t
g) forall (m :: k).
Ob m =>
ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
kk =
    f s b
-> g b t
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (s ~> (m ** b)) -> ((m ** b) ~> t) -> r)
-> r
forall (s :: k) (a :: k) (b :: k) (t :: k) r.
SymMonoidal k =>
f s a
-> g b t
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) r.
(MonLensFl p q, SymMonoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP f s b
f g b t
g \ @(mo :: k) ComonoidOn m
co s ~> (m ** b)
ho (m ** b) ~> t
io ->
      f' b a
-> g' b b
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (b ~> (m ** a)) -> ((m ** b) ~> b) -> r)
-> r
forall (s :: k) (a :: k) (b :: k) (t :: k) r.
SymMonoidal k =>
f' s a
-> g' b t
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) r.
(MonLensFl p q, SymMonoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP f' b a
f' g' b b
g' \ @(mi :: k) ComonoidOn m
ci b ~> (m ** a)
hi (m ** b) ~> b
ii ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @mo @mi
          ( forall (m :: k).
Ob m =>
ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
kk @(mo ** mi)
              (ComonoidOn m -> ComonoidOn m -> ComonoidOn (m ** m)
forall {k} (a :: k) (b :: k).
SymMonoidal k =>
ComonoidOn a -> ComonoidOn b -> ComonoidOn (a ** b)
tensorComonoid ComonoidOn m
co ComonoidOn m
ci)
              (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @mo @mi @afoc ((m ** (m ** a)) ~> ((m ** m) ** a))
-> (s ~> (m ** (m ** a))) -> s ~> ((m ** m) ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @mo Obj m -> (b ~> (m ** a)) -> (m ** b) ~> (m ** (m ** 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 ~> (m ** a)
hi) ((m ** b) ~> (m ** (m ** a)))
-> (s ~> (m ** b)) -> s ~> (m ** (m ** a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (m ** b)
ho)
              ((m ** b) ~> t
io ((m ** b) ~> t)
-> (((m ** m) ** b) ~> (m ** b)) -> ((m ** m) ** b) ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @mo Obj m -> ((m ** b) ~> b) -> (m ** (m ** b)) ~> (m ** 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
ii) ((m ** (m ** b)) ~> (m ** b))
-> (((m ** m) ** b) ~> (m ** (m ** b)))
-> ((m ** m) ** b) ~> (m ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @mo @mi @bfoc)
          )

type MonoidalLens (s :: k) (t :: k) a b = Optic (Prostrong MonLensFl) s t a b
type MonoidalLens' s a = MonoidalLens s s a a

-- | Build a monoidal lens from its two legs and a chosen __comonoidal__ residual @m@.
monLens
  :: forall {k} (m :: k) (s :: k) t a b
   . (Comonoid m, Ob a, Ob b) => (s ~> m ** a) -> (m ** b ~> t) -> MonoidalLens s t a b
monLens :: forall {k} (m :: k) (s :: k) (t :: k) (a :: k) (b :: k).
(Comonoid m, Ob a, Ob b) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonoidalLens s t a b
monLens s ~> (m ** a)
h (m ** b) ~> t
i = 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 @MonLensFl (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)
h) (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
i)

-- | Eliminate any optic that is at least an iso and at most a monoidal lens to its two legs,
-- recovering the existential residual @m@ together with its comonoid structure: run it at its
-- witness pair ('ExOptic' 'MonLensFl', via 'withLegs') and read the legs off with 'withMonLensP'.
withMonLens
  :: forall {k} c (s :: k) (t :: k) a b r
   . (SymMonoidal k, (Ob a, Ob b) => c (ExOptic MonLensFl a b))
  => Optic c s t a b -> (forall m. (Ob m) => ComonoidOn m -> (s ~> m ** a) -> (m ** b ~> t) -> r) -> r
withMonLens :: forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (t :: k)
       (a :: k) (b :: k) r.
(SymMonoidal k, (Ob a, Ob b) => c (ExOptic MonLensFl a b)) =>
Optic c s t a b
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLens Optic c s t a b
o forall (m :: k).
Ob m =>
ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k = 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 @MonLensFl Optic c s t a b
o \ @p @q p s a
p q b t
q -> forall {k} (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) r.
(MonLensFl p q, SymMonoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (a :: k) (b :: k)
       (t :: k) r.
(MonLensFl p q, SymMonoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP @p @q p s a
p q b t
q \ @m ComonoidOn m
co s ~> (m ** a)
h (m ** b) ~> t
i -> forall (m :: k).
Ob m =>
ComonoidOn m -> (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k @m ComonoidOn m
co s ~> (m ** a)
h (m ** b) ~> t
i