{-# 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 @m@ is carried through the tensor, and being a 'Comonoid' it can be /discarded/
-- (@'counit' :: m ~> 'Unit'@) and /copied/ -- which is exactly what a lens's @get@ needs. So a
-- monoidal lens is a genuine lens (it views, sets, folds and traverses), and it sits below
-- 'Proarrow.Optic.MonoidalTraversal.MonoidalTraversal' and 'Proarrow.Optic.Getter.Getter' in the
-- lattice, mirroring the ordinary 'Proarrow.Optic.Lens.Lens' below
-- 'Proarrow.Optic.AffineTraversal.AffineTraversal':
--
-- > Lens         <: { Getter, AffineTraversal }      -- product residual
-- > MonoidalLens <: { Getter, MonoidalTraversal }    -- comonoidal tensor residual
--
-- Crucially it asks 'Comonoid' of __the residual only__, not
-- 'Proarrow.Category.Monoidal.CopyDiscard.CopyDiscard' of the whole category: it works in every
-- @CopyDiscard@ category (there every object is a comonoid) /and/ in genuinely non-cartesian ones
-- like @LINEAR@ for the residuals that are comonoids (the duplicable @Ur@ objects). The ordinary
-- 'Proarrow.Optic.Lens.Lens' is the @tensor = product@ specialization, where the residual is
-- recoverable from @s@ by projection.
module Proarrow.Optic.MonoidalLens where

import Proarrow.Adjunction (Proadjunction (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), Tensor)
import Proarrow.Category.Monoidal.Strength (Strong (..))
import Proarrow.Colimit.BinaryCoproduct (lft)
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (\\), type (+->))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (Comonoid)
import Proarrow.Monoid qualified as Mon
import Proarrow.Optic
  ( ExOptic (..)
  , FLAVOR
  , Optic
  , Optic_ (..)
  , Prostrong (..)
  , SubFlavor (..)
  , ex2prof
  )
import Proarrow.Optic.AffineFold (AffineFoldRes (..))
import Proarrow.Optic.Fold (FoldRes (..))
import Proarrow.Optic.Getter (GetterRes (..))
import Proarrow.Optic.Setter (SetterRes (..))
import Proarrow.Optic.Traversal (MonTravRes (..), TravRes (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))

-- | Witness pair for a monoidal lens: the focus @a@ sits inside @m ** a@ with a __comonoidal__
-- residual @m@. Being a comonoid, @m@ can be discarded (for @get@\/fold) and carried (for @set@).
type LensW :: forall {k}. k -> k +-> k
data LensW m s a where
  LensW :: (Comonoid m, Ob a) => (s ~> (m ** a)) -> LensW m s a

-- | The covariant half of the 'LensW' witness pair: the set leg, @(m '**' b) '~>' t@.
type CoLensW :: forall {k}. k -> k +-> k
data CoLensW m b t where
  CoLensW :: (Comonoid m, Ob b) => ((m ** b) ~> t) -> CoLensW m b t

instance (Comonoid (m :: k)) => Profunctor (LensW m :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> LensW m a b -> LensW m c d
dimap c ~> a
l b ~> d
r (LensW a ~> (m ** b)
h) = (c ~> (m ** d)) -> LensW m c d
forall {k} (m :: k) (a :: k) (s :: k).
(Comonoid m, Ob a) =>
(s ~> (m ** a)) -> LensW m s a
LensW ((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m Obj m -> (b ~> d) -> (m ** b) ~> (m ** d)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** b ~> d
r) ((m ** b) ~> (m ** d)) -> (c ~> (m ** b)) -> c ~> (m ** d)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (m ** b)
h (a ~> (m ** b)) -> (c ~> a) -> c ~> (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
. c ~> a
l) ((Ob b, Ob d) => LensW m c d) -> (b ~> d) -> LensW m c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> LensW m a b -> r
\\ LensW a ~> (m ** b)
h = r
(Ob a, Ob b) => r
(Ob a, Ob (m ** b)) => r
r ((Ob a, Ob (m ** b)) => r) -> (a ~> (m ** b)) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> (m ** b)
h
instance (Comonoid (m :: k)) => Profunctor (CoLensW m :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> CoLensW m a b -> CoLensW m c d
dimap c ~> a
l b ~> d
r (CoLensW (m ** a) ~> b
i) = ((m ** c) ~> d) -> CoLensW m c d
forall {k} (m :: k) (b :: k) (t :: k).
(Comonoid m, Ob b) =>
((m ** b) ~> t) -> CoLensW m b t
CoLensW (b ~> d
r (b ~> d) -> ((m ** c) ~> b) -> (m ** c) ~> d
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (m ** a) ~> b
i ((m ** a) ~> b) -> ((m ** c) ~> (m ** a)) -> (m ** c) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m Obj m -> (c ~> a) -> (m ** c) ~> (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)
** c ~> a
l)) ((Ob c, Ob a) => CoLensW m c d) -> (c ~> a) -> CoLensW m c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c ~> a
l
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> CoLensW m a b -> r
\\ CoLensW (m ** a) ~> b
i = r
(Ob a, Ob b) => r
(Ob (m ** a), Ob b) => r
r ((Ob (m ** a), Ob b) => r) -> ((m ** a) ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (m ** a) ~> b
i

instance (Comonoid (m :: k)) => Proadjunction (LensW m :: k +-> k) (CoLensW m) where
  unit :: forall (a :: k). Ob a => (:.:) (CoLensW m) (LensW m) a a
unit @c = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @m @c (((m ** a) ~> (m ** a)) -> CoLensW m a (m ** a)
forall {k} (m :: k) (b :: k) (t :: k).
(Comonoid m, Ob b) =>
((m ** b) ~> t) -> CoLensW m b t
CoLensW (m ** a) ~> (m ** a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id CoLensW m a (m ** a)
-> LensW m (m ** a) a -> (:.:) (CoLensW m) (LensW m) a a
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ((m ** a) ~> (m ** a)) -> LensW m (m ** a) a
forall {k} (m :: k) (a :: k) (s :: k).
(Comonoid m, Ob a) =>
(s ~> (m ** a)) -> LensW m s a
LensW (m ** a) ~> (m ** a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id)
  counit :: (LensW m :.: CoLensW m) :~> (~>)
counit (LensW a ~> (m ** b)
h :.: CoLensW (m ** b) ~> b
i) = (m ** b) ~> b
i ((m ** b) ~> b) -> (a ~> (m ** b)) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> (m ** b)
h
instance (Comonoid (m :: k)) => SetterRes (LensW m :: k +-> k) (CoLensW m) where
  overP :: forall (s :: k) (a :: k) (b :: k) (t :: k).
LensW m s a -> CoLensW m b t -> (a ~> b) -> s ~> t
overP (LensW s ~> (m ** a)
h) (CoLensW (m ** b) ~> t
i) a ~> b
f = (m ** b) ~> t
i ((m ** b) ~> t) -> (s ~> (m ** b)) -> s ~> t
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @m Obj m -> (a ~> b) -> (m ** a) ~> (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)
** a ~> b
f) ((m ** a) ~> (m ** b)) -> (s ~> (m ** a)) -> s ~> (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
. s ~> (m ** a)
h
instance (Comonoid (m :: k)) => FoldRes (LensW m :: k +-> k) (CoLensW m) where
  foldMapP :: forall (m :: k) (s :: k) (a :: k).
Monoid m =>
LensW m s a -> (a ~> m) -> s ~> m
foldMapP (LensW s ~> (m ** a)
h) a ~> m
am = (Unit ** m) ~> m
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((Unit ** m) ~> m) -> (s ~> (Unit ** m)) -> s ~> m
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
Mon.counit @m (m ~> Unit) -> (a ~> m) -> (m ** a) ~> (Unit ** m)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** a ~> m
am) ((m ** a) ~> (Unit ** m)) -> (s ~> (m ** a)) -> s ~> (Unit ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (m ** a)
h
instance (Comonoid (m :: k)) => AffineFoldRes (LensW m :: k +-> k) (CoLensW m) where
  previewP :: forall (s :: k) (a :: k).
Bicartesian k =>
LensW m s a -> s ~> (a || TerminalObject)
previewP @_ @a (LensW s ~> (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 :: k +-> 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 :: 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 ~> 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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (m ** a)
h
instance (Comonoid (m :: k)) => GetterRes (LensW m :: k +-> k) (CoLensW m) where
  getP :: forall (s :: k) (a :: k). LensW m s a -> s ~> a
getP @_ @a (LensW s ~> (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 :: 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 ~> 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 :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. s ~> (m ** a)
h
instance (Comonoid (m :: k)) => TravRes (LensW m :: k +-> k) (CoLensW m)
instance (Comonoid (m :: k)) => MonTravRes (LensW m :: k +-> k) (CoLensW m) where
  monTravP :: forall (r :: k +-> k) (s :: k) (a :: k) (b :: k) (t :: k).
StrongDistributiveProfunctor r =>
LensW m s a -> CoLensW m b t -> r a b -> r s t
monTravP (LensW s ~> (m ** a)
h) (CoLensW (m ** b) ~> t
i) r a b
r = (s ~> (m ** a)) -> ((m ** b) ~> t) -> r (m ** a) (m ** b) -> r s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> r a b -> r c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap s ~> (m ** a)
h (m ** b) ~> t
i (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (k, k) +-> k) (p :: k +-> k) (a :: k) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @Tensor @_ @m r a b
r)

-- | The monoidal-lens flavor: a lens whose residual is a comonoid, so it is both a
-- 'Proarrow.Optic.Getter.Getter' and a 'Proarrow.Optic.MonoidalTraversal.MonoidalTraversal'.
type MonLensRes :: forall {k}. FLAVOR k k
class (GetterRes p q, MonTravRes p q) => MonLensRes (p :: k +-> k) (q :: k +-> k) where
  -- | Recover a monoidal lens's two legs, with the (comonoidal) residual @m@ existential.
  withMonLensP :: (Monoidal k) => p s a -> q b t -> (forall (m :: k). (Ob m) => (s ~> m ** a) -> (m ** b ~> t) -> r) -> r

instance (Comonoid (m :: k)) => MonLensRes (LensW m :: k +-> k) (CoLensW m) where
  withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
LensW m s a
-> CoLensW m b t
-> (forall (m :: k).
    Ob m =>
    (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP (LensW s ~> (m ** a)
h) (CoLensW (m ** b) ~> t
i) forall (m :: k). Ob m => (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k = forall (m :: k). Ob m => (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k @m s ~> (m ** a)
h (m ** b) ~> t
i

instance (CategoryOf k) => MonLensRes (Id :: k +-> k) (Id :: k +-> k) where
  withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
Id s a
-> Id b t
-> (forall (m :: k).
    Ob m =>
    (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP (Id s ~> a
sa) (Id b ~> t
bt) forall (m :: k). Ob m => (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k = forall (m :: k). Ob m => (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k @Unit (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
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 :: 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
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)
   . (MonLensRes f g, MonLensRes f' g')
  => MonLensRes (f :.: f') (g' :.: g)
  where
  withMonLensP :: forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
(:.:) f f' s a
-> (:.:) g' g b t
-> (forall (m :: k).
    Ob m =>
    (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP (f s b
f :.: (f' b a
f' :: f' hix afoc)) ((g' b b
g' :: g' bfoc giy) :.: g b t
g) forall (m :: k). Ob m => (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
kk =
    f s b
-> g b t
-> (forall (m :: k).
    Ob m =>
    (s ~> (m ** b)) -> ((m ** b) ~> t) -> r)
-> r
forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
f s a
-> g b t
-> (forall (m :: k).
    Ob 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.
(MonLensRes p q, Monoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP f s b
f g b t
g \ @(mo :: k) s ~> (m ** b)
ho (m ** b) ~> t
io ->
      f' b a
-> g' b b
-> (forall (m :: k).
    Ob m =>
    (b ~> (m ** a)) -> ((m ** b) ~> b) -> r)
-> r
forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
f' s a
-> g' b t
-> (forall (m :: k).
    Ob 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.
(MonLensRes p q, Monoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP f' b a
f' g' b b
g' \ @(mi :: k) 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 => (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
kk @(mo ** mi)
              (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 :: 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 @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 :: k +-> 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 :: 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 @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 :: 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 @mo @mi @bfoc)
          )
          ((Ob b, Ob a) => r) -> f' b a -> r
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' b a
f'
          ((Ob b, Ob b) => r) -> g' b b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> g' 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
\\ g' b b
g'

instance SubFlavor MonLensRes GetterRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
MonLensRes p q =>
(GetterRes p q => r) -> r
subFlavor GetterRes p q => r
r = r
GetterRes p q => r
r
instance SubFlavor MonLensRes MonTravRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
MonLensRes p q =>
(MonTravRes p q => r) -> r
subFlavor MonTravRes p q => r
r = r
MonTravRes p q => r
r
instance SubFlavor MonLensRes TravRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
MonLensRes p q =>
(TravRes p q => r) -> r
subFlavor TravRes p q => r
r = r
TravRes p q => r
r
instance SubFlavor MonLensRes SetterRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
MonLensRes p q =>
(SetterRes p q => r) -> r
subFlavor SetterRes p q => r
r = r
SetterRes p q => r
r
instance SubFlavor MonLensRes AffineFoldRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
MonLensRes p q =>
(AffineFoldRes p q => r) -> r
subFlavor AffineFoldRes p q => r
r = r
AffineFoldRes p q => r
r
instance SubFlavor MonLensRes FoldRes where subFlavor :: forall (p :: j +-> j) (q :: j +-> j) r.
MonLensRes p q =>
(FoldRes p q => r) -> r
subFlavor FoldRes p q => r
r = r
FoldRes p q => r
r

type MonoidalLens (s :: k) (t :: k) a b = Optic (Prostrong MonLensRes) 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 = ExOptic MonLensRes a b s t -> Optic (Prostrong MonLensRes) s t a b
forall {j} {k} {w :: FLAVOR j k} (a :: k) (b :: j) (s :: k)
       (t :: j).
(CategoryOf j, CategoryOf k) =>
ExOptic w a b s t -> Optic (Prostrong w) s t a b
ex2prof (forall {j} {k} {w :: FLAVOR j k} (p :: k +-> k) (q :: j +-> j)
       (s :: k) (t :: j) (a :: k) (b :: j).
(w p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic w a b) q s t -> ExOptic w a b s t
forall (p :: k +-> k) (q :: k +-> k) (s :: k) (t :: k) (a :: k)
       (b :: k).
(MonLensRes p q, Profunctor p, Profunctor q) =>
(:.:) (p :.: ExOptic MonLensRes a b) q s t
-> ExOptic MonLensRes a b s t
ExProstrong @(LensW m) @(CoLensW m) ((s ~> (m ** a)) -> LensW m s a
forall {k} (m :: k) (a :: k) (s :: k).
(Comonoid m, Ob a) =>
(s ~> (m ** a)) -> LensW m s a
LensW s ~> (m ** a)
h LensW m s a
-> ExOptic MonLensRes a b a b
-> (:.:) (LensW m) (ExOptic MonLensRes a b) s b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (a ~> a) -> (b ~> b) -> ExOptic MonLensRes a b a b
forall {j} {k} {w :: FLAVOR j k} (s :: k) (t :: j) (a :: k)
       (b :: j).
(s ~> a) -> (b ~> t) -> ExOptic w a b s t
ExIso a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (:.:) (LensW m) (ExOptic MonLensRes a b) s b
-> CoLensW m b t
-> (:.:) (LensW m :.: ExOptic MonLensRes a b) (CoLensW m) s t
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ((m ** b) ~> t) -> CoLensW m b t
forall {k} (m :: k) (b :: k) (t :: k).
(Comonoid m, Ob b) =>
((m ** b) ~> t) -> CoLensW m b t
CoLensW (m ** b) ~> t
i))

-- | The eliminating carrier for monoidal lenses: the two legs with the residual @m@ existential.
type MonShop :: forall {k}. k -> k -> k +-> k
data MonShop a b s t where
  MonShop :: (Ob a, Ob b, Ob m) => (s ~> m ** a) -> (m ** b ~> t) -> MonShop a b s t

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

-- | Any flavor whose optics have monoidal-lens legs has strength for the 'MonShop' carrier:
-- absorbing a witness pair combines its residual with the carrier's by tensoring.
instance (Monoidal k, Ob (a :: k), Ob b, SubFlavor w MonLensRes) => Prostrong (w :: FLAVOR k k) (MonShop a b :: k +-> k) where
  proact :: forall (f :: k +-> k) (g :: k +-> k).
(w f g, Profunctor f, Profunctor g) =>
((f :.: MonShop a b) :.: g) :~> MonShop a b
proact @f @g (f a b
f :.: MonShop @_ @_ @m b ~> (m ** a)
h (m ** b) ~> b
i :.: g b b
g) =
    forall {j} {k} (w1 :: FLAVOR j k) (w2 :: FLAVOR j k) (p :: k +-> k)
       (q :: j +-> j) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
forall (w1 :: FLAVOR k k) (w2 :: FLAVOR k k) (p :: k +-> k)
       (q :: k +-> k) r.
(SubFlavor w1 w2, w1 p q) =>
(w2 p q => r) -> r
subFlavor @w @MonLensRes @f @g
      ( f a b
-> g b b
-> (forall (m :: k).
    Ob m =>
    (a ~> (m ** b)) -> ((m ** b) ~> b) -> MonShop a b a b)
-> MonShop a b a b
forall (s :: k) (a :: k) (b :: k) (t :: k) r.
Monoidal k =>
f s a
-> g b t
-> (forall (m :: k).
    Ob 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.
(MonLensRes p q, Monoidal k) =>
p s a
-> q b t
-> (forall (m :: k).
    Ob m =>
    (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLensP f a b
f g b b
g \ @mf a ~> (m ** b)
hf (m ** b) ~> b
ir ->
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @mf @m
            ( forall (a :: k) (b :: k) (m :: k) (s :: k) (t :: k).
(Ob a, Ob b, Ob m) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonShop a b s t
forall {k} (a :: k) (b :: k) (m :: k) (s :: k) (t :: k).
(Ob a, Ob b, Ob m) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonShop a b s t
MonShop @a @b @(mf ** m)
                (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @mf @m @a ((m ** (m ** a)) ~> ((m ** m) ** a))
-> (a ~> (m ** (m ** a))) -> a ~> ((m ** m) ** 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 @mf 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)
h) ((m ** b) ~> (m ** (m ** a)))
-> (a ~> (m ** b)) -> a ~> (m ** (m ** 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
. a ~> (m ** b)
hf)
                ((m ** b) ~> b
ir ((m ** b) ~> b)
-> (((m ** m) ** b) ~> (m ** b)) -> ((m ** m) ** b) ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @mf 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
i) ((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 :: 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 @mf @m @b)
            )
      )

-- | Eliminate any optic that is at least an iso and at most a monoidal lens to its two legs,
-- recovering the existential residual @m@.
withMonLens
  :: forall {k} c (s :: k) (t :: k) a b r
   . (Monoidal k, (Ob a, Ob b) => c (MonShop a b))
  => Optic c s t a b -> (forall m. (Ob 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.
(Monoidal k, (Ob a, Ob b) => c (MonShop a b)) =>
Optic c s t a b
-> (forall (m :: k).
    Ob m =>
    (s ~> (m ** a)) -> ((m ** b) ~> t) -> r)
-> r
withMonLens (Optic forall (p :: k +-> k). c p => p a b -> p s t
l) forall (m :: k). Ob m => (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k = case forall (p :: k +-> k). c p => p a b -> p s t
l @(MonShop a b) (forall (a :: k) (b :: k) (m :: k) (s :: k) (t :: k).
(Ob a, Ob b, Ob m) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonShop a b s t
forall {k} (a :: k) (b :: k) (m :: k) (s :: k) (t :: k).
(Ob a, Ob b, Ob m) =>
(s ~> (m ** a)) -> ((m ** b) ~> t) -> MonShop a b s t
MonShop @a @b @Unit a ~> (Unit ** a)
a ~> (Unit ** a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv (Unit ** b) ~> b
(Unit ** b) ~> b
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor) of
  MonShop @_ @_ @m s ~> (m ** a)
h (m ** b) ~> t
i -> forall (m :: k). Ob m => (s ~> (m ** a)) -> ((m ** b) ~> t) -> r
k @m s ~> (m ** a)
s ~> (m ** a)
h (m ** b) ~> t
(m ** b) ~> t
i