Some strong monoidal action action

Author: sjoerdvisscher

src/Proarrow/Category/Instance/Cat.hs

@@ -38,7 +38,7 @@ import Proarrow.Object.Exponential (Closed (..))
 import Proarrow.Object.Initial (HasInitialObject (..))
 import Proarrow.Object.Terminal (HasTerminalObject (..))
 import Proarrow.Profunctor.Composition ((:.:))
-import Proarrow.Profunctor.Identity (Id)
+import Proarrow.Profunctor.Identity (Id (..))
 import Proarrow.Profunctor.Representable (Rep, Representable (..))
 
 newtype KIND = K Kind
@@ -232,8 +232,8 @@ instance MonoidalAction KIND KIND where
   multiplicator = associatorInv
   multiplicatorInv = associator
 
-instance Strong KIND Cat where
-  act = par
+instance Strong KIND (Id :: CAT KIND) where
+  act = par . Id
 
 instance Costrong KIND Cat where
   coact @u = compactClosedCoact @u

src/Proarrow/Category/Instance/Kleisli.hs

@@ -11,6 +11,8 @@ module Proarrow.Category.Instance.Kleisli
   , pattern LiftF
   ) where
 
+import Data.Kind (Type)
+
 import Proarrow.Adjunction (Proadjunction)
 import Proarrow.Adjunction qualified as Adj
 import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
@@ -38,6 +40,7 @@ import Proarrow.Profunctor.Representable (RepCostar(..), Representable(..), triv
 import Proarrow.Monoid (CopyDiscard (..))
 import Proarrow.Category.Enriched.ThinCategory qualified as T
 import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
+import Proarrow.Profunctor.Identity (Id (..))
 
 newtype KLEISLI (p :: CAT k) = KL k
 type instance UN KL (KL k) = k
@@ -115,15 +118,15 @@ instance (Distributive k, Promonad p, DistributiveProfunctor p) => Distributive
   distL0 @(KL a) = arr (distL0 @k @a)
   distR0 @(KL a) = arr (distR0 @k @a)
 
-instance (Strong k p, Promonad p, Monoidal k) => Strong k (Kleisli :: CAT (KLEISLI (p :: k +-> k))) where
-  act f (Kleisli p) = Kleisli (act f p)
-instance (Strong k p, Promonad p, Monoidal k) => MonoidalAction k (KLEISLI (p :: k +-> k)) where
+instance (Strong Type p, Promonad p) => Strong Type (Id :: CAT (KLEISLI (p :: Type +-> Type))) where
+  act f (Id (Kleisli p)) = Id (Kleisli (act f p))
+instance (Strong Type p, Promonad p) => MonoidalAction Type (KLEISLI (p :: Type +-> Type)) where
   type Act y (KL x) = KL (Act y x)
-  withObAct @y @(KL x) r = withObAct @k @k @y @x r
-  unitor = arr (unitor @k)
-  unitorInv = arr (unitorInv @k)
-  multiplicator @a @b @(KL c) = arr (multiplicator @k @k @a @b @c)
-  multiplicatorInv @a @b @(KL c) = arr (multiplicatorInv @k @k @a @b @c)
+  withObAct @y @(KL x) r = withObAct @Type @Type @y @x r
+  unitor = arr (unitor @Type)
+  unitorInv = arr (unitorInv @Type)
+  multiplicator @a @b @(KL c) = arr (multiplicator @Type @Type @a @b @c)
+  multiplicatorInv @a @b @(KL c) = arr (multiplicatorInv @Type @Type @a @b @c)
 
 instance (DaggerProfunctor p, Promonad p) => DaggerProfunctor (Kleisli :: CAT (KLEISLI p)) where
   dagger (Kleisli p) = Kleisli (dagger p)

src/Proarrow/Category/Instance/Linear.hs

@@ -12,7 +12,7 @@ import Proarrow.Category.Monoidal.Action (Costrong (..))
 import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, type (+->))
 import Proarrow.Functor (Functor (..), FunctorForRep (..))
 import Proarrow.Monoid (Comonoid (..))
-import Proarrow.Object.BinaryCoproduct (COPROD, Coprod (..), HasBinaryCoproducts (..))
+import Proarrow.Object.BinaryCoproduct (COPROD, HasBinaryCoproducts (..))
 import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
 import Proarrow.Object.Copower (Copowered (..))
 import Proarrow.Object.Dual (StarAutonomous (..))
@@ -22,7 +22,6 @@ import Proarrow.Object.Power (Powered (..))
 import Proarrow.Object.Terminal (HasTerminalObject (..))
 import Proarrow.Profunctor.Composition ((:.:) (..))
 import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..))
-import Proarrow.Profunctor.Identity (Id (..))
 import Proarrow.Profunctor.Representable (Rep (..))
 import System.IO.Unsafe (unsafeDupablePerformIO)
 import Unsafe.Coerce (unsafeCoerce)
@@ -127,8 +126,8 @@ instance HasInitialObject LINEAR where
   type InitialObject = L Void
   initiate = Linear \case {}
 
-instance Costrong (COPROD LINEAR) (Coprod (Id :: CAT LINEAR)) where
-  coact (Coprod (Id (Linear uxuy))) = Coprod (Id (loop . Linear Right))
+instance Costrong (COPROD LINEAR) Linear where
+  coact (Linear uxuy) = loop . Linear Right
     where
       loop = Linear \ux -> case uxuy ux of Left x -> unLinear loop (Left x); Right b -> b
 

src/Proarrow/Category/Instance/Mat.hs

@@ -25,6 +25,7 @@ import Proarrow.Object.Dual
 import Proarrow.Object.Exponential (Closed (..))
 import Proarrow.Object.Initial (HasInitialObject (..))
 import Proarrow.Object.Terminal (HasTerminalObject (..))
+import Proarrow.Profunctor.Identity (Id(..))
 
 type data Nat = Z | S Nat
 
@@ -224,8 +225,8 @@ instance (P.Num a) => MonoidalAction (MatK a) (MatK a) where
   multiplicator @(M b) @(M c) @(M d) = withAssocMult @d @c @b (obj @(M b) `par` (obj @(M c) `par` obj @(M d)))
   multiplicatorInv @(M b) @(M c) @(M d) = withAssocMult @d @c @b (obj @(M b) `par` (obj @(M c) `par` obj @(M d)))
 
-instance (P.Num a) => Strong (MatK a) (Mat :: CAT (MatK a)) where
-  act = par
+instance (P.Num a) => Strong (MatK a) (Id :: CAT (MatK a)) where
+  act = par . Id
 
 instance (P.Num a) => Costrong (MatK a) (Mat :: CAT (MatK a)) where
   coact @x = compactClosedCoact @x

src/Proarrow/Category/Instance/Nat.hs

@@ -27,6 +27,7 @@ import Proarrow.Object.Initial (HasInitialObject (..))
 import Proarrow.Object.Power (Powered (..))
 import Proarrow.Object.Terminal (HasTerminalObject (..))
 import Proarrow.Profunctor.Composition ((:.:) (..))
+import Proarrow.Profunctor.Identity (Id (..))
 
 type Nat :: CAT (j -> k)
 data Nat f g where
@@ -114,8 +115,8 @@ instance Monoidal (Type -> Type) where
   associator = Nat (Compose . map Compose . getCompose . getCompose)
   associatorInv = Nat (Compose . Compose . map getCompose . getCompose)
 
-instance Strong (Type -> Type) (->) where
-  act (Nat n) f = n . map f
+instance Strong (Type -> Type) (Id :: CAT Type) where
+  act (Nat n) (Id f) = Id (n . map f)
 instance MonoidalAction (Type -> Type) Type where
   type Act (p :: Type -> Type) (x :: Type) = p x
   withObAct r = r

src/Proarrow/Category/Instance/Sub.hs

@@ -10,6 +10,7 @@ import Proarrow.Functor (FunctorForRep (..))
 import Proarrow.Monoid (CopyDiscard (..))
 import Proarrow.Profunctor.Corepresentable (Corepresentable)
 import Proarrow.Profunctor.Representable (Representable (..))
+import Proarrow.Profunctor.Identity (Id)
 
 type SUBCAT :: forall {k}. OB k -> Type
 type data SUBCAT (ob :: OB k) = SUB k
@@ -70,11 +71,11 @@ instance (Representable p, forall a. (ob a) => ob (p % a)) => Representable (Sub
   tabulate (Sub f) = Sub (tabulate f)
   repMap (Sub f) = Sub (repMap @p f)
 
-instance (MonoidalAction m Type, Monoidal (SUBCAT (ob :: OB m))) => Strong (SUBCAT (ob :: OB m)) (->) where
+instance (MonoidalAction m k, Monoidal (SUBCAT (ob :: OB m))) => Strong (SUBCAT (ob :: OB m)) (Id :: CAT k) where
   Sub f `act` g = f `act` g
-instance (MonoidalAction m Type, Monoidal (SUBCAT (ob :: OB m))) => MonoidalAction (SUBCAT (ob :: OB m)) Type where
-  type Act (p :: SUBCAT ob) (x :: Type) = Act (UN SUB p) x
-  withObAct r = r
+instance (MonoidalAction m k, Monoidal (SUBCAT (ob :: OB m))) => MonoidalAction (SUBCAT (ob :: OB m)) k where
+  type Act (p :: SUBCAT ob) (x :: k) = Act (UN SUB p) x
+  withObAct @(SUB a) @x r = withObAct @m @k @a @x r
   unitor = unitor @m
   unitorInv = unitorInv @m
   multiplicator @(SUB p) @(SUB q) @x = multiplicator @_ @_ @p @q @x

src/Proarrow/Category/Monoidal/Action.hs

@@ -5,9 +5,13 @@ module Proarrow.Category.Monoidal.Action where
 import Data.Kind (Constraint)
 import Prelude (type (~))
 
+import Proarrow.Category.Instance.Product ((:**:) (..))
+import Proarrow.Category.Instance.Unit qualified as U
 import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
 import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), obj, type (+->))
-import Proarrow.Category.Instance.Product ((:**:) (..))
+import Proarrow.Profunctor.Identity (Id (..))
+import Proarrow.Profunctor.Representable (Representable (..), trivialRep)
+import Proarrow.Profunctor.Corepresentable (Corepresentable(..), trivialCorep)
 
 -- | Profuntorial strength for a monoidal action.
 -- Gives functorial strength for representable profunctors,
@@ -16,9 +20,16 @@ type Strong :: forall {j} {k}. Kind -> j +-> k -> Constraint
 class (MonoidalAction m c, MonoidalAction m d, Profunctor p) => Strong m (p :: c +-> d) where
   act :: forall (a :: m) b x y. a ~> b -> p x y -> p (Act a x) (Act b y)
 
+actHom :: (MonoidalAction m k) => (a :: m) ~> b -> (x :: k) ~> y -> Act a x ~> Act b y
+actHom ab xy = unId (act ab (Id xy))
+
+instance (Profunctor p) => Strong () p where
+  act U.Unit p = p
+
 instance (Strong m p, Strong m' q) => Strong (m, m') (p :**: q) where
   act (p :**: q) (x :**: y) = act p x :**: act q y
-class (Monoidal m, CategoryOf k, Strong m ((~>) :: CAT k)) => MonoidalAction m k where
+
+class (Monoidal m, CategoryOf k, Strong m (Id :: CAT k)) => MonoidalAction m k where
   -- I would like to default Act to `**`, but that doesn't seem possible without GHC thinking `m` and `k` are the same.
   type Act (a :: m) (x :: k) :: k
   withObAct :: (Ob (a :: m), Ob (x :: k)) => ((Ob (Act a x)) => r) -> r
@@ -27,6 +38,17 @@ class (Monoidal m, CategoryOf k, Strong m ((~>) :: CAT k)) => MonoidalAction m k
   multiplicator :: (Ob (a :: m), Ob (b :: m), Ob (x :: k)) => Act a (Act b x) ~> Act (a ** b) x
   multiplicatorInv :: (Ob (a :: m), Ob (b :: m), Ob (x :: k)) => Act (a ** b) x ~> Act a (Act b x)
 
+instance (CategoryOf k) => MonoidalAction () k where
+  type Act '() x = x
+  withObAct r = r
+  unitor = id
+  unitorInv = id
+  multiplicator = id
+  multiplicatorInv = id
+
+instance (Strong m (Id :: CAT p), Strong n (Id :: CAT q)) => Strong (m, n) (Id :: CAT (p, q)) where
+  act (f :**: f') (Id (g :**: g')) = Id (actHom f g :**: actHom f' g')
+
 instance (MonoidalAction n j, MonoidalAction m k) => MonoidalAction (n, m) (j, k) where
   type Act '(p, q) '(x, y) = '(Act p x, Act q y)
   withObAct @'(p, q) @'(x, y) r = withObAct @n @j @p @x (withObAct @m @k @q @y r)
@@ -35,7 +57,6 @@ instance (MonoidalAction n j, MonoidalAction m k) => MonoidalAction (n, m) (j, k
   multiplicator @'(p, q) @'(r, s) @'(x, y) = multiplicator @n @j @p @r @x :**: multiplicator @m @k @q @s @y
   multiplicatorInv @'(p, q) @'(r, s) @'(x, y) = multiplicatorInv @n @j @p @r @x :**: multiplicatorInv @m @k @q @s @y
 
-
 class (MonoidalAction m k, SymMonoidal m) => SymMonoidalAction m k
 instance (MonoidalAction m k, SymMonoidal m) => SymMonoidalAction m k
 
@@ -57,37 +78,46 @@ instance
   => SelfAction k
 
 toSelfAct :: forall {k} (a :: k) b. (SelfAction k, Ob a, Ob b) => a ** b ~> Act a b
-toSelfAct = obj @a `act` obj @b
+toSelfAct = unId (obj @a `act` Id (obj @b))
 
 fromSelfAct :: forall {k} (a :: k) b. (SelfAction k, Ob a, Ob b) => Act a b ~> a ** b
-fromSelfAct = obj @a `act` obj @b
+fromSelfAct = unId (obj @a `act` Id (obj @b))
 
 composeActs
   :: forall {m} {k} (x :: m) y (c :: k) a b
    . (MonoidalAction m k, Ob x, Ob y, Ob c)
   => a ~> Act x b
   -> b ~> Act y c
   -> a ~> Act (x ** y) c
-composeActs f g = multiplicator @m @k @x @y @c . act (obj @x) g . f
+composeActs f g = multiplicator @m @k @x @y @c . actHom (obj @x) g . f
 
 decomposeActs
   :: forall {m} {k} (x :: m) y (c :: k) a b
    . (MonoidalAction m k, Ob x, Ob y, Ob c)
   => Act y c ~> b
   -> Act x b ~> a
   -> Act (x ** y) c ~> a
-decomposeActs f g = g . act (obj @x) f . multiplicatorInv @m @k @x @y @c
+decomposeActs f g = g . actHom (obj @x) f . multiplicatorInv @m @k @x @y @c
 
 first' :: forall {k} {p :: CAT k} c a b. (SelfAction k, Strong k p, Ob c) => p a b -> p (a ** c) (b ** c)
 first' p = dimap (swap @k @a @c) (swap @k @c @b) (second' @c p) \\ p
 
 second' :: forall {k} {p :: CAT k} c a b. (SelfAction k, Strong k p, Ob c) => p a b -> p (c ** a) (c ** b)
 second' p = act (obj @c) p
 
+-- | If a strong profunctor is representable, we get the usual strength for the represented functor.
+strength :: forall {m} p a b. (Representable p, Strong m p, Ob (a :: m), Ob b) => Act a (p % b) ~> p % Act a b
+strength = index (act (obj @a) (trivialRep @p @b))
+
+-- | If a strong profunctor is corepresentable, we get the usual costrength for the represented functor.
+costrength :: forall {m} p a b. (Corepresentable p, Strong m p, Ob (a :: m), Ob b) => p %% Act a b ~> Act a (p %% b)
+costrength = coindex (act (obj @a) (trivialCorep @p @b))
+
 -- | This is not monoidal `par` but premonoidal, i.e. no sliding.
 -- So with `prepar f g` the effects of f happen before the effects of g.
 -- p needs to be a commutative promonad for this to be monoidal `par`.
-prepar :: forall {k} {p :: CAT k} a b c d. (SelfAction k, Strong k p, Promonad p) => p a b -> p c d -> p (a ** c) (b ** d)
+prepar
+  :: forall {k} {p :: CAT k} a b c d. (SelfAction k, Strong k p, Promonad p) => p a b -> p c d -> p (a ** c) (b ** d)
 prepar f g = second' @b g . first' @c f \\ f \\ g
 
 strongPar0 :: forall {k} {p :: CAT k} a. (SelfAction k, Strong k p, MonoidalProfunctor p, Ob a) => p a a

src/Proarrow/Category/Monoidal/Optic.hs

@@ -1,27 +1,27 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE IncoherentInstances #-}
-{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -Wno-orphans -fprint-potential-instances #-}
 
 module Proarrow.Category.Monoidal.Optic where
 
 import Data.Bifunctor (bimap)
 import Data.Kind (Type)
-import Prelude (Either, Maybe (..), Monad (..), Traversable, const, either, fmap, fst, snd, uncurry, ($), type (~))
+import Prelude (Either (..), Maybe (..), Monad (..), Traversable, const, either, fmap, uncurry, ($), type (~))
 
 import Proarrow.Category.Instance.Kleisli (KLEISLI (..), Kleisli (..))
 import Proarrow.Category.Instance.Nat ((!))
-import Proarrow.Category.Instance.Product ((:**:) (..))
 import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
 import Proarrow.Category.Monoidal (MonoidalProfunctor (..), SymMonoidal, swap)
-import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..), composeActs, decomposeActs)
+import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..), composeActs, decomposeActs, actHom)
 import Proarrow.Category.Opposite (OPPOSITE (..))
 import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), dimapDefault, obj, type (+->))
+import Proarrow.Core qualified as Core
 import Proarrow.Functor (Prelude (..))
 import Proarrow.Object (src, tgt)
 import Proarrow.Object.BinaryCoproduct (COPROD (..), Coprod (..))
-import Proarrow.Object.BinaryProduct ()
+import Proarrow.Object.BinaryProduct (Cartesian, HasBinaryProducts (..))
+import Proarrow.Profunctor.Identity (Id (..))
 import Proarrow.Profunctor.Star (Star, pattern Star)
-import Proarrow.Profunctor.Identity (Id(..))
 
 type Optic :: Kind -> c -> d -> c -> d -> Type
 data Optic m a b s t where
@@ -42,13 +42,10 @@ instance (CategoryOf c, CategoryOf d) => Profunctor (Optic m a b :: c +-> d) whe
 instance (IsOptic m c d) => Strong m (Optic m a b :: c +-> d) where
   act :: forall (a1 :: m) (b1 :: m) (s :: d) (t :: c). a1 ~> b1 -> Optic m a b s t -> Optic m a b (Act a1 s) (Act b1 t)
   act w (Optic @x @x' f w' g) =
-    Optic (composeActs @a1 @x @a (src w `act` src f) f) (w `par` w') (decomposeActs @b1 @x' @b g (tgt w `act` tgt g))
+    Optic (composeActs @a1 @x @a (src w `actHom` src f) f) (w `par` w') (decomposeActs @b1 @x' @b g (tgt w `actHom` tgt g))
       \\ w
       \\ w'
 
-parallel :: Optic m a b s t -> Optic m' c d u v -> Optic (m, m') '(a, c) '(b, d) '(s, u) '(t, v)
-parallel (Optic f w g) (Optic h w' i) = Optic (f :**: h) (w :**: w') (g :**: i)
-
 type data OPTIC m (c :: Kind) (d :: Kind) = OPT c d
 type family OptL (p :: OPTIC w c d) where
   OptL (OPT c d) = c
@@ -64,30 +61,36 @@ instance (IsOptic m c d) => Profunctor (OpticCat :: CAT (OPTIC m c d)) where
 instance (IsOptic m c d) => Promonad (OpticCat :: CAT (OPTIC m c d)) where
   id = OpticCat (prof2ex id)
   OpticCat l@Optic{} . OpticCat r@Optic{} = OpticCat $ prof2ex (ex2prof l . ex2prof r)
+
 -- | The category of optics.
 instance (IsOptic m c d) => CategoryOf (OPTIC m c d) where
   type (~>) = OpticCat
   type Ob a = (a ~ OPT (OptL a) (OptR a), Ob (OptL a), Ob (OptR a))
 
-type MixedOptic m a b s t = forall p. (Strong m p) => p a b -> p s t
+type MixedOptic m a b s t = Core.Optic (Strong m) s t a b
+
+toIso :: MixedOptic () a b s t -> Core.Iso s t a b
+toIso l p = l p
 
 ex2prof :: forall m a b s t. Optic m a b s t -> MixedOptic m a b s t
 ex2prof (Optic l w r) p = dimap l r (act w p)
 
 prof2ex
-  :: forall {c} {d} m a b s t
+  :: forall {c} {d} m (a :: c) (b :: d) (s :: c) (t :: d)
    . (MonoidalAction m c, MonoidalAction m d, Ob a, Ob b)
-  => MixedOptic m (a :: c) (b :: d) (s :: c) (t :: d)
+  => MixedOptic m a b s t
   -> Optic m a b s t
 prof2ex p2p = p2p (Optic (unitorInv @m) par0 (unitor @m))
 
-type Lens s t a b = MixedOptic Type a b s t
-mkLens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
-mkLens sa sbt = ex2prof (Optic (\s -> (s, sa s)) (src sa) (uncurry sbt))
+type Lens (s :: k) t a b = MixedOptic k a b s t
+mkLens
+  :: (Cartesian k, Act s a ~ (s && a), Act s b ~ (s && b), Ob (b :: k))
+  => (s ~> a) -> ((s && b) ~> t) -> Lens s t a b
+mkLens sa sbt = ex2prof (Optic (id &&& sa) (src sa) sbt) \\ sa
 
-type Prism s t a b = MixedOptic (COPROD Type) (COPR a) (COPR b) (COPR s) (COPR t)
+type Prism (s :: k) t a b = MixedOptic (COPROD k) a b s t
 mkPrism :: (s -> Either t a) -> (b -> t) -> Prism s t a b
-mkPrism sat bt = ex2prof @(COPROD Type) (Optic (Coprod (Id sat)) id (Coprod (Id (either id bt))))
+mkPrism sta bt = ex2prof @(COPROD Type) (Optic sta id (either id bt))
 
 type Traversal s t a b = MixedOptic (SUBCAT Traversable) a b s t
 traversing :: (Traversable f) => Traversal (f a) (f b) a b
@@ -113,10 +116,10 @@ infixl 8 ^.
 (^.) :: s -> (Viewing a b a b -> Viewing a b s t) -> a
 (^.) s l = unView (l $ Viewing id) s
 
-data Previewing a (b :: COPROD Type) s (t :: COPROD Type) where
-  Previewing :: {unPreview :: s -> Maybe a} -> Previewing (COPR a) (COPR b) (COPR s) (COPR t)
+data Previewing a (b :: Type) s (t :: Type) where
+  Previewing :: {unPreview :: s -> Maybe a} -> Previewing a b s t
 instance Profunctor (Previewing a b) where
-  dimap (Coprod (Id l)) Coprod{} (Previewing f) = Previewing (f . l)
+  dimap l _ (Previewing f) = Previewing (f . l)
   r \\ Previewing f = r \\ f
 instance Strong (COPROD Type) (Previewing a b) where
   act _ (Previewing f) = Previewing (either (const Nothing) f)
@@ -125,7 +128,7 @@ instance Strong Type (Previewing a b) where
 
 infixl 8 ?.
 (?.)
-  :: s -> (Previewing (COPR a) (COPR b) (COPR a) (COPR b) -> Previewing (COPR a) (COPR b) (COPR s) (COPR t)) -> Maybe a
+  :: s -> (Previewing a b a b -> Previewing a b s t) -> Maybe a
 (?.) s l = unPreview (l $ Previewing Just) s
 
 type KlCat m = KLEISLI (Star (Prelude m))
@@ -193,9 +196,10 @@ instance (IsChart m c d) => Promonad (ChartCat :: CAT (CHART m c d)) where
   id = ChartCat (prof2ex id)
   ChartCat (Optic @x @x' @_ @t ll lw lr) . ChartCat (Optic @y @y' @a rl rw rr) =
     ChartCat $
-      Optic (composeActs @x @y @a ll rl) (lw `par` rw) (decomposeActs @y' @x' @t lr rr . (swap @_ @x' @y' `act` obj @t))
+      Optic (composeActs @x @y @a ll rl) (lw `par` rw) (decomposeActs @y' @x' @t lr rr . (swap @_ @x' @y' `actHom` obj @t))
         \\ lw
         \\ rw
+
 -- | The category of charts.
 instance (IsChart m c d) => CategoryOf (CHART m c d) where
   type (~>) = ChartCat