{-# LANGUAGE AllowAmbiguousTypes, IncoherentInstances #-}
module Proarrow.Category.Monoidal.Optic where

import Data.Kind (Constraint, Type)
import Data.Bifunctor (bimap)
import Data.Functor.Identity (Identity (..))
import Data.Functor.Compose (Compose (..))
import Prelude (uncurry, Either, either, fst, snd, ($), Maybe (..), const, Traversable, Monad (..), fmap)

import Proarrow.Core (CategoryOf (..), PRO, Profunctor (..), Promonad (..), UN, OB, Kind, CAT, dimapDefault, (:~>))
import Proarrow.Category.Monoidal (Monoidal(..), MonoidalProfunctor (..))
import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Functor (Functor(..), Prelude (..))
import Proarrow.Object (Obj, obj, src, tgt)
import Proarrow.Object.BinaryCoproduct (COPROD(..), Coprod (..), mkCoprod)
import Proarrow.Object.BinaryProduct ()
import Proarrow.Category.Instance.Sub (SUBCAT(..), Sub (..))
import Proarrow.Category.Instance.Kleisli (KLEISLI(..), Kleisli(..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Profunctor.Day (Day(..), DayUnit (..))
import Proarrow.Profunctor.Star (Star(..))
import Proarrow.Category.Instance.Prof (Prof(..))
import Proarrow.Monoid (Monoid)
import Proarrow.Profunctor.Yoneda (Yo (..))


class (Monoidal m, CategoryOf k) => MonoidalAction m k where
  type Act (p :: m) (x :: k) :: k
  act :: (p :: m) ~> q -> (x :: k) ~> y -> Act p x ~> Act q y
  unitor :: Obj (x :: k) -> Act (Unit :: m) x ~> x
  unitorInv :: Obj (x :: k) -> x ~> Act (Unit :: m) x
  multiplicator :: Obj (p :: m) -> Obj (q :: m) -> Obj (x :: k) -> Act p (Act q x) ~> Act (p ** q) x
  multiplicatorInv :: Obj (p :: m) -> Obj (q :: m) -> Obj (x :: k) -> Act (p ** q) x ~> Act p (Act q x)

instance MonoidalAction Type Type where
  type Act p x = p ** x
  act :: forall p q x y. (p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act = (p ~> q) -> (x ~> y) -> (p ** x) ~> (q ** y)
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall a b c d. (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
par
  unitor :: forall x. Obj x -> Act Unit x ~> x
unitor = Obj x -> (Unit ** x) ~> x
Obj x -> Act Unit x ~> x
forall a. Obj a -> (Unit ** a) ~> a
forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a
leftUnitor
  unitorInv :: forall x. Obj x -> x ~> Act Unit x
unitorInv = Obj x -> x ~> (Unit ** x)
Obj x -> x ~> Act Unit x
forall a. Obj a -> a ~> (Unit ** a)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
leftUnitorInv
  multiplicator :: forall p q x.
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator = Obj p -> Obj q -> Obj x -> (p ** (q ** x)) ~> ((p ** q) ** x)
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b c.
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv
  multiplicatorInv :: forall p q x.
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv = Obj p -> Obj q -> Obj x -> ((p ** q) ** x) ~> (p ** (q ** x))
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b c.
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator

instance MonoidalAction (COPROD Type) (COPROD Type) where
  type Act p x = p ** x
  act :: forall (p :: COPROD Type) (q :: COPROD Type) (x :: COPROD Type)
       (y :: COPROD Type).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act = (p ~> q) -> (x ~> y) -> (p ** x) ~> (q ** y)
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall (a :: COPROD Type) (b :: COPROD Type) (c :: COPROD Type)
       (d :: COPROD Type).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
par
  unitor :: forall (x :: COPROD Type). Obj x -> Act Unit x ~> x
unitor = Obj x -> (Unit ** x) ~> x
Obj x -> Act Unit x ~> x
forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a
forall (a :: COPROD Type). Obj a -> (Unit ** a) ~> a
leftUnitor
  unitorInv :: forall (x :: COPROD Type). Obj x -> x ~> Act Unit x
unitorInv = Obj x -> x ~> (Unit ** x)
Obj x -> x ~> Act Unit x
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
forall (a :: COPROD Type). Obj a -> a ~> (Unit ** a)
leftUnitorInv
  multiplicator :: forall (p :: COPROD Type) (q :: COPROD Type) (x :: COPROD Type).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator = Obj p -> Obj q -> Obj x -> (p ** (q ** x)) ~> ((p ** q) ** x)
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall (a :: COPROD Type) (b :: COPROD Type) (c :: COPROD Type).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv
  multiplicatorInv :: forall (p :: COPROD Type) (q :: COPROD Type) (x :: COPROD Type).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv = Obj p -> Obj q -> Obj x -> ((p ** q) ** x) ~> (p ** (q ** x))
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: COPROD Type) (b :: COPROD Type) (c :: COPROD Type).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator

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)
  act :: forall (p :: (n, m)) (q :: (n, m)) (x :: (j, k)) (y :: (j, k)).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act (a1 ~> b1
p :**: a2 ~> b2
q) (a1 ~> b1
x :**: a2 ~> b2
y) = (a1 ~> b1) -> (a1 ~> b1) -> Act a1 a1 ~> Act b1 b1
forall (p :: n) (q :: n) (x :: j) (y :: j).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act a1 ~> b1
p a1 ~> b1
x (Act a1 a1 ~> Act b1 b1)
-> (Act a2 a2 ~> Act b2 b2)
-> (:**:) (~>) (~>) '(Act a1 a1, Act a2 a2) '(Act b1 b1, Act b2 b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> b2) -> (a2 ~> b2) -> Act a2 a2 ~> Act b2 b2
forall (p :: m) (q :: m) (x :: k) (y :: k).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act a2 ~> b2
q a2 ~> b2
y
  unitor :: forall (x :: (j, k)). Obj x -> Act Unit x ~> x
unitor (a1 ~> b1
x :**: a2 ~> b2
y) = forall m k (x :: k). MonoidalAction m k => Obj x -> Act Unit x ~> x
unitor @n a1 ~> b1
Obj b1
x (Act Unit b1 ~> b1)
-> (Act Unit b2 ~> b2)
-> (:**:) (~>) (~>) '(Act Unit b1, Act Unit b2) '(b1, b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall m k (x :: k). MonoidalAction m k => Obj x -> Act Unit x ~> x
unitor @m a2 ~> b2
Obj b2
y
  unitorInv :: forall (x :: (j, k)). Obj x -> x ~> Act Unit x
unitorInv (a1 ~> b1
x :**: a2 ~> b2
y) = forall m k (x :: k). MonoidalAction m k => Obj x -> x ~> Act Unit x
unitorInv @n a1 ~> b1
Obj b1
x (b1 ~> Act Unit b1)
-> (b2 ~> Act Unit b2)
-> (:**:) (~>) (~>) '(b1, b2) '(Act Unit b1, Act Unit b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall m k (x :: k). MonoidalAction m k => Obj x -> x ~> Act Unit x
unitorInv @m a2 ~> b2
Obj b2
y
  multiplicator :: forall (p :: (n, m)) (q :: (n, m)) (x :: (j, k)).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator (a1 ~> b1
p :**: a2 ~> b2
q) (a1 ~> b1
r :**: a2 ~> b2
s) (a1 ~> b1
x :**: a2 ~> b2
y) = Obj b1
-> Obj b1 -> Obj b1 -> Act b1 (Act b1 b1) ~> Act (b1 ** b1) b1
forall (p :: n) (q :: n) (x :: j).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator a1 ~> b1
Obj b1
p a1 ~> b1
Obj b1
r a1 ~> b1
Obj b1
x (Act b1 (Act b1 b1) ~> Act (b1 ** b1) b1)
-> (Act b2 (Act b2 b2) ~> Act (b2 ** b2) b2)
-> (:**:)
     (~>)
     (~>)
     '(Act b1 (Act b1 b1), Act b2 (Act b2 b2))
     '(Act (b1 ** b1) b1, Act (b2 ** b2) b2)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Obj b2
-> Obj b2 -> Obj b2 -> Act b2 (Act b2 b2) ~> Act (b2 ** b2) b2
forall (p :: m) (q :: m) (x :: k).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator a2 ~> b2
Obj b2
q a2 ~> b2
Obj b2
s a2 ~> b2
Obj b2
y
  multiplicatorInv :: forall (p :: (n, m)) (q :: (n, m)) (x :: (j, k)).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv (a1 ~> b1
p :**: a2 ~> b2
q) (a1 ~> b1
r :**: a2 ~> b2
s) (a1 ~> b1
x :**: a2 ~> b2
y) = Obj b1
-> Obj b1 -> Obj b1 -> Act (b1 ** b1) b1 ~> Act b1 (Act b1 b1)
forall (p :: n) (q :: n) (x :: j).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv a1 ~> b1
Obj b1
p a1 ~> b1
Obj b1
r a1 ~> b1
Obj b1
x (Act (b1 ** b1) b1 ~> Act b1 (Act b1 b1))
-> (Act (b2 ** b2) b2 ~> Act b2 (Act b2 b2))
-> (:**:)
     (~>)
     (~>)
     '(Act (b1 ** b1) b1, Act (b2 ** b2) b2)
     '(Act b1 (Act b1 b1), Act b2 (Act b2 b2))
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Obj b2
-> Obj b2 -> Obj b2 -> Act (b2 ** b2) b2 ~> Act b2 (Act b2 b2)
forall (p :: m) (q :: m) (x :: k).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv a2 ~> b2
Obj b2
q a2 ~> b2
Obj b2
s a2 ~> b2
Obj b2
y

instance MonoidalAction Type (COPROD Type) where
  type Act (p :: Type) (COPR x :: COPROD Type) = COPR (p ** x)
  p ~> q
l act :: forall p q (x :: COPROD Type) (y :: COPROD Type).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
`act` Coprod UN 'COPR x ~> UN 'COPR y
r = (UN 'COPR ('COPR (p, UN 'COPR x))
 ~> UN 'COPR ('COPR (q, UN 'COPR y)))
-> Coprod ('COPR (p, UN 'COPR x)) ('COPR (q, UN 'COPR y))
forall {k} (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(UN 'COPR a ~> UN 'COPR b) -> Coprod a b
Coprod (p ~> q
l (p ~> q)
-> (UN 'COPR x ~> UN 'COPR y)
-> (p ** UN 'COPR x) ~> (q ** UN 'COPR y)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall a b c d. (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` UN 'COPR x ~> UN 'COPR y
r)
  unitor :: forall (x :: COPROD Type). Obj x -> Act Unit x ~> x
unitor (Coprod UN 'COPR x ~> UN 'COPR x
x) = (UN 'COPR ('COPR ((), UN 'COPR x))
 ~> UN 'COPR ('COPR (UN 'COPR x)))
-> Coprod ('COPR ((), UN 'COPR x)) ('COPR (UN 'COPR x))
forall {k} (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(UN 'COPR a ~> UN 'COPR b) -> Coprod a b
Coprod ((UN 'COPR x ~> UN 'COPR x) -> (Unit ** UN 'COPR x) ~> UN 'COPR x
forall a. Obj a -> (Unit ** a) ~> a
forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a
leftUnitor UN 'COPR x ~> UN 'COPR x
x)
  unitorInv :: forall (x :: COPROD Type). Obj x -> x ~> Act Unit x
unitorInv (Coprod UN 'COPR x ~> UN 'COPR x
x) = (UN 'COPR ('COPR (UN 'COPR x))
 ~> UN 'COPR ('COPR ((), UN 'COPR x)))
-> Coprod ('COPR (UN 'COPR x)) ('COPR ((), UN 'COPR x))
forall {k} (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(UN 'COPR a ~> UN 'COPR b) -> Coprod a b
Coprod ((UN 'COPR x ~> UN 'COPR x) -> UN 'COPR x ~> (Unit ** UN 'COPR x)
forall a. Obj a -> a ~> (Unit ** a)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
leftUnitorInv UN 'COPR x ~> UN 'COPR x
x)
  multiplicator :: forall p q (x :: COPROD Type).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator Obj p
p Obj q
q (Coprod UN 'COPR x ~> UN 'COPR x
x) = (UN 'COPR ('COPR (p, (q, UN 'COPR x)))
 ~> UN 'COPR ('COPR ((p, q), UN 'COPR x)))
-> Coprod ('COPR (p, (q, UN 'COPR x))) ('COPR ((p, q), UN 'COPR x))
forall {k} (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(UN 'COPR a ~> UN 'COPR b) -> Coprod a b
Coprod (Obj p
-> Obj q
-> (UN 'COPR x ~> UN 'COPR x)
-> (p ** (q ** UN 'COPR x)) ~> ((p ** q) ** UN 'COPR x)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b c.
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj p
p Obj q
q UN 'COPR x ~> UN 'COPR x
x)
  multiplicatorInv :: forall p q (x :: COPROD Type).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv Obj p
p Obj q
q (Coprod UN 'COPR x ~> UN 'COPR x
x) = (UN 'COPR ('COPR ((p, q), UN 'COPR x))
 ~> UN 'COPR ('COPR (p, (q, UN 'COPR x))))
-> Coprod ('COPR ((p, q), UN 'COPR x)) ('COPR (p, (q, UN 'COPR x)))
forall {k} (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(UN 'COPR a ~> UN 'COPR b) -> Coprod a b
Coprod (Obj p
-> Obj q
-> (UN 'COPR x ~> UN 'COPR x)
-> ((p ** q) ** UN 'COPR x) ~> (p ** (q ** UN 'COPR x))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b c.
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Obj p
p Obj q
q UN 'COPR x ~> UN 'COPR x
x)

instance MonoidalAction (COPROD Type) Type where
  type Act (p :: COPROD Type) (x :: Type) = UN COPR (p ** COPR x)
  f :: p ~> q
f@Coprod{} act :: forall (p :: COPROD Type) (q :: COPROD Type) x y.
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
`act` x ~> y
g = Coprod
  ('COPR
     (Either (UN 'COPR ('COPR (UN 'COPR p))) (UN 'COPR ('COPR x))))
  ('COPR
     (Either (UN 'COPR ('COPR (UN 'COPR q))) (UN 'COPR ('COPR y))))
-> UN
     'COPR
     ('COPR
        (Either (UN 'COPR ('COPR (UN 'COPR p))) (UN 'COPR ('COPR x))))
   ~> UN
        'COPR
        ('COPR
           (Either (UN 'COPR ('COPR (UN 'COPR q))) (UN 'COPR ('COPR y))))
forall {j} (a :: COPROD j) (b :: COPROD j).
Coprod a b -> UN 'COPR a ~> UN 'COPR b
getCoprod (p ~> q
'COPR (UN 'COPR p) ~> 'COPR (UN 'COPR q)
f ('COPR (UN 'COPR p) ~> 'COPR (UN 'COPR q))
-> ('COPR x ~> 'COPR y)
-> ('COPR (UN 'COPR p) ** 'COPR x)
   ~> ('COPR (UN 'COPR q) ** 'COPR y)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall (a :: COPROD Type) (b :: COPROD Type) (c :: COPROD Type)
       (d :: COPROD Type).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` (x ~> y) -> Coprod ('COPR x) ('COPR y)
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Coprod ('COPR a) ('COPR b)
mkCoprod x ~> y
g)
  unitor :: forall x. Obj x -> Act Unit x ~> x
unitor Obj x
x = Coprod ('COPR (Either Void x)) ('COPR x)
-> UN 'COPR ('COPR (Either Void x)) ~> UN 'COPR ('COPR x)
forall {j} (a :: COPROD j) (b :: COPROD j).
Coprod a b -> UN 'COPR a ~> UN 'COPR b
getCoprod (Obj ('COPR x) -> (Unit ** 'COPR x) ~> 'COPR x
forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a
forall (a :: COPROD Type). Obj a -> (Unit ** a) ~> a
leftUnitor ((UN 'COPR ('COPR x) ~> UN 'COPR ('COPR x))
-> Coprod ('COPR x) ('COPR x)
forall {k} (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(UN 'COPR a ~> UN 'COPR b) -> Coprod a b
Coprod Obj x
UN 'COPR ('COPR x) ~> UN 'COPR ('COPR x)
x))
  unitorInv :: forall x. Obj x -> x ~> Act Unit x
unitorInv Obj x
x = Coprod ('COPR x) ('COPR (Either Void (UN 'COPR ('COPR x))))
-> UN 'COPR ('COPR x)
   ~> UN 'COPR ('COPR (Either Void (UN 'COPR ('COPR x))))
forall {j} (a :: COPROD j) (b :: COPROD j).
Coprod a b -> UN 'COPR a ~> UN 'COPR b
getCoprod (Obj ('COPR x) -> 'COPR x ~> (Unit ** 'COPR x)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
forall (a :: COPROD Type). Obj a -> a ~> (Unit ** a)
leftUnitorInv ((UN 'COPR ('COPR x) ~> UN 'COPR ('COPR x))
-> Coprod ('COPR x) ('COPR x)
forall {k} (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(UN 'COPR a ~> UN 'COPR b) -> Coprod a b
Coprod Obj x
UN 'COPR ('COPR x) ~> UN 'COPR ('COPR x)
x))
  multiplicator :: forall (p :: COPROD Type) (q :: COPROD Type) x.
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator p :: Obj p
p@Coprod{} q :: Obj q
q@Coprod{} Obj x
x = Coprod
  ('COPR (Either (UN 'COPR p) (Either (UN 'COPR q) x)))
  ('COPR
     (Either
        (Either
           (UN 'COPR ('COPR (UN 'COPR p))) (UN 'COPR ('COPR (UN 'COPR q))))
        (UN 'COPR ('COPR x))))
-> UN 'COPR ('COPR (Either (UN 'COPR p) (Either (UN 'COPR q) x)))
   ~> UN
        'COPR
        ('COPR
           (Either
              (Either
                 (UN 'COPR ('COPR (UN 'COPR p))) (UN 'COPR ('COPR (UN 'COPR q))))
              (UN 'COPR ('COPR x))))
forall {j} (a :: COPROD j) (b :: COPROD j).
Coprod a b -> UN 'COPR a ~> UN 'COPR b
getCoprod (Obj ('COPR (UN 'COPR p))
-> Obj ('COPR (UN 'COPR q))
-> Obj ('COPR x)
-> ('COPR (UN 'COPR p) ** ('COPR (UN 'COPR q) ** 'COPR x))
   ~> (('COPR (UN 'COPR p) ** 'COPR (UN 'COPR q)) ** 'COPR x)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall (a :: COPROD Type) (b :: COPROD Type) (c :: COPROD Type).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Obj p
Obj ('COPR (UN 'COPR p))
p Obj q
Obj ('COPR (UN 'COPR q))
q (Obj x -> Coprod ('COPR x) ('COPR x)
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Coprod ('COPR a) ('COPR b)
mkCoprod Obj x
x))
  multiplicatorInv :: forall (p :: COPROD Type) (q :: COPROD Type) x.
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv p :: Obj p
p@Coprod{} q :: Obj q
q@Coprod{} Obj x
x = Coprod
  ('COPR (Either (Either (UN 'COPR p) (UN 'COPR q)) x))
  ('COPR
     (Either
        (UN 'COPR ('COPR (UN 'COPR p)))
        (Either (UN 'COPR ('COPR (UN 'COPR q))) (UN 'COPR ('COPR x)))))
-> UN 'COPR ('COPR (Either (Either (UN 'COPR p) (UN 'COPR q)) x))
   ~> UN
        'COPR
        ('COPR
           (Either
              (UN 'COPR ('COPR (UN 'COPR p)))
              (Either (UN 'COPR ('COPR (UN 'COPR q))) (UN 'COPR ('COPR x)))))
forall {j} (a :: COPROD j) (b :: COPROD j).
Coprod a b -> UN 'COPR a ~> UN 'COPR b
getCoprod (Obj ('COPR (UN 'COPR p))
-> Obj ('COPR (UN 'COPR q))
-> Obj ('COPR x)
-> (('COPR (UN 'COPR p) ** 'COPR (UN 'COPR q)) ** 'COPR x)
   ~> ('COPR (UN 'COPR p) ** ('COPR (UN 'COPR q) ** 'COPR x))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: COPROD Type) (b :: COPROD Type) (c :: COPROD Type).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Obj p
Obj ('COPR (UN 'COPR p))
p Obj q
Obj ('COPR (UN 'COPR q))
q (Obj x -> Coprod ('COPR x) ('COPR x)
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> Coprod ('COPR a) ('COPR b)
mkCoprod Obj x
x))

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
  act :: forall (p :: SUBCAT ob) (q :: SUBCAT ob) (x :: k) (y :: k).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act (Sub a1 ~> b1
f) x ~> y
g = a1 ~> b1
f (a1 ~> b1) -> (x ~> y) -> Act a1 x ~> Act b1 y
forall (p :: m) (q :: m) (x :: k) (y :: k).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
`act` x ~> y
g
  unitor :: forall (x :: k). Obj x -> Act Unit x ~> x
unitor = forall m k (x :: k). MonoidalAction m k => Obj x -> Act Unit x ~> x
unitor @m
  unitorInv :: forall (x :: k). Obj x -> x ~> Act Unit x
unitorInv = forall m k (x :: k). MonoidalAction m k => Obj x -> x ~> Act Unit x
unitorInv @m
  multiplicator :: forall (p :: SUBCAT ob) (q :: SUBCAT ob) (x :: k).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator (Sub a1 ~> b1
p) (Sub a1 ~> b1
q) = Obj b1
-> Obj b1 -> (x ~> x) -> Act b1 (Act b1 x) ~> Act (b1 ** b1) x
forall (p :: m) (q :: m) (x :: k).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator a1 ~> b1
Obj b1
p a1 ~> b1
Obj b1
q
  multiplicatorInv :: forall (p :: SUBCAT ob) (q :: SUBCAT ob) (x :: k).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv (Sub a1 ~> b1
p) (Sub a1 ~> b1
q) = Obj b1
-> Obj b1 -> (x ~> x) -> Act (b1 ** b1) x ~> Act b1 (Act b1 x)
forall (p :: m) (q :: m) (x :: k).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv a1 ~> b1
Obj b1
p a1 ~> b1
Obj b1
q

instance MonoidalAction (Type -> Type) Type where
  type Act (p :: Type -> Type) (x :: Type) = p x
  act :: forall (p :: Type -> Type) (q :: Type -> Type) x y.
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act (Nat p .~> q
n) x ~> y
f = p y ~> q y
p y -> q y
p .~> q
n (p y -> q y) -> (p x -> p y) -> p x -> q y
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x ~> y) -> p x ~> p y
forall a b. (a ~> b) -> p a ~> p b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map x ~> y
f
  unitor :: forall x. Obj x -> Act Unit x ~> x
unitor Obj x
_ = Act Unit x ~> x
Identity x -> x
forall a. Identity a -> a
runIdentity
  unitorInv :: forall x. Obj x -> x ~> Act Unit x
unitorInv Obj x
_ = x ~> Act Unit x
x -> Identity x
forall a. a -> Identity a
Identity
  multiplicator :: forall (p :: Type -> Type) (q :: Type -> Type) x.
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator Obj p
_ Obj q
_ Obj x
_ = Act p (Act q x) ~> Act (p ** q) x
p (q x) -> Compose p q x
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose
  multiplicatorInv :: forall (p :: Type -> Type) (q :: Type -> Type) x.
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv Obj p
_ Obj q
_ Obj x
_ = Act (p ** q) x ~> Act p (Act q x)
Compose p q x -> p (q x)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose

instance Monad m => MonoidalAction Type (KlCat m) where
  type Act (p :: Type) (KL x :: KlCat m) = KL (p ** x)
  p ~> q
l act :: forall p q (x :: KlCat m) (y :: KlCat m).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
`act` Kleisli (Star a1 ~> Prelude m b1
r) = Star (Prelude m) (p, a1) (q, b1)
-> Kleisli ('KL (p, a1)) ('KL (q, b1))
forall {k} (p :: CAT k) (a1 :: k) (b1 :: k).
p a1 b1 -> Kleisli ('KL a1) ('KL b1)
Kleisli (((p, a1) ~> Prelude m (q, b1)) -> Star (Prelude m) (p, a1) (q, b1)
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star (\(p
p, a1
a) -> (b1 ~> (q, b1)) -> Prelude m b1 ~> Prelude m (q, b1)
forall a b. (a ~> b) -> Prelude m a ~> Prelude m b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map (p ~> q
p -> q
l p
p,) (a1 ~> Prelude m b1
a1 -> Prelude m b1
r a1
a)))
  unitor :: forall (x :: KlCat m). Obj x -> Act Unit x ~> x
unitor (Kleisli (Star a1 ~> Prelude m b1
f)) = Star (Prelude m) ((), b1) b1 -> Kleisli ('KL ((), b1)) ('KL b1)
forall {k} (p :: CAT k) (a1 :: k) (b1 :: k).
p a1 b1 -> Kleisli ('KL a1) ('KL b1)
Kleisli ((((), b1) ~> Prelude m b1) -> Star (Prelude m) ((), b1) b1
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star (m b1 -> Prelude m b1
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude (m b1 -> Prelude m b1)
-> (((), b1) -> m b1) -> ((), b1) -> Prelude m b1
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. b1 -> m b1
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (b1 -> m b1) -> (((), b1) -> b1) -> ((), b1) -> m b1
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall m k (x :: k). MonoidalAction m k => Obj x -> Act Unit x ~> x
unitor @Type ((b1 -> Prelude m b1) -> Obj b1
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a1 ~> Prelude m b1
b1 -> Prelude m b1
f)))
  unitorInv :: forall (x :: KlCat m). Obj x -> x ~> Act Unit x
unitorInv (Kleisli (Star a1 ~> Prelude m b1
f)) = Star (Prelude m) b1 ((), b1) -> Kleisli ('KL b1) ('KL ((), b1))
forall {k} (p :: CAT k) (a1 :: k) (b1 :: k).
p a1 b1 -> Kleisli ('KL a1) ('KL b1)
Kleisli ((b1 ~> Prelude m ((), b1)) -> Star (Prelude m) b1 ((), b1)
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star (m ((), b1) -> Prelude m ((), b1)
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude (m ((), b1) -> Prelude m ((), b1))
-> (b1 -> m ((), b1)) -> b1 -> Prelude m ((), b1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((), b1) -> m ((), b1)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (((), b1) -> m ((), b1)) -> (b1 -> ((), b1)) -> b1 -> m ((), b1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall m k (x :: k). MonoidalAction m k => Obj x -> x ~> Act Unit x
unitorInv @Type ((b1 -> Prelude m b1) -> Obj b1
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a1 ~> Prelude m b1
b1 -> Prelude m b1
f)))
  multiplicator :: forall p q (x :: KlCat m).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator Obj p
p Obj q
q (Kleisli (Star a1 ~> Prelude m b1
f)) = Star (Prelude m) (p, (q, b1)) ((p, q), b1)
-> Kleisli ('KL (p, (q, b1))) ('KL ((p, q), b1))
forall {k} (p :: CAT k) (a1 :: k) (b1 :: k).
p a1 b1 -> Kleisli ('KL a1) ('KL b1)
Kleisli (((p, (q, b1)) ~> Prelude m ((p, q), b1))
-> Star (Prelude m) (p, (q, b1)) ((p, q), b1)
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star (m ((p, q), b1) -> Prelude m ((p, q), b1)
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude (m ((p, q), b1) -> Prelude m ((p, q), b1))
-> ((p, (q, b1)) -> m ((p, q), b1))
-> (p, (q, b1))
-> Prelude m ((p, q), b1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((p, q), b1) -> m ((p, q), b1)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (((p, q), b1) -> m ((p, q), b1))
-> ((p, (q, b1)) -> ((p, q), b1)) -> (p, (q, b1)) -> m ((p, q), b1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator @Type Obj p
p Obj q
q ((b1 -> Prelude m b1) -> Obj b1
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a1 ~> Prelude m b1
b1 -> Prelude m b1
f)))
  multiplicatorInv :: forall p q (x :: KlCat m).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv Obj p
p Obj q
q (Kleisli (Star a1 ~> Prelude m b1
f)) = Star (Prelude m) ((p, q), b1) (p, (q, b1))
-> Kleisli ('KL ((p, q), b1)) ('KL (p, (q, b1)))
forall {k} (p :: CAT k) (a1 :: k) (b1 :: k).
p a1 b1 -> Kleisli ('KL a1) ('KL b1)
Kleisli ((((p, q), b1) ~> Prelude m (p, (q, b1)))
-> Star (Prelude m) ((p, q), b1) (p, (q, b1))
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star (m (p, (q, b1)) -> Prelude m (p, (q, b1))
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude (m (p, (q, b1)) -> Prelude m (p, (q, b1)))
-> (((p, q), b1) -> m (p, (q, b1)))
-> ((p, q), b1)
-> Prelude m (p, (q, b1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (p, (q, b1)) -> m (p, (q, b1))
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((p, (q, b1)) -> m (p, (q, b1)))
-> (((p, q), b1) -> (p, (q, b1))) -> ((p, q), b1) -> m (p, (q, b1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv @Type Obj p
p Obj q
q ((b1 -> Prelude m b1) -> Obj b1
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a1 ~> Prelude m b1
b1 -> Prelude m b1
f)))



-- | "Day convolaction"
data DayAct w p a b where
  DayAct :: forall w p a b c d e f. a ~> Act c e -> w c d -> p e f -> Act d f ~> b -> DayAct w p a b

instance (Profunctor w, Profunctor p) => Profunctor (DayAct (w :: PRO m m') (p :: PRO c d)) where
  dimap :: forall (c :: c) (a :: c) (b :: d) (d :: d).
(c ~> a) -> (b ~> d) -> DayAct w p a b -> DayAct w p c d
dimap c ~> a
l b ~> d
r (DayAct a ~> Act c e
f w c d
w p e f
p Act d f ~> b
g) = (c ~> Act c e)
-> w c d -> p e f -> (Act d f ~> d) -> DayAct w p c d
forall {k} {m} {k} {k} (w :: k -> m -> Type) (p :: k -> k -> Type)
       (a :: k) (b :: k) (b :: k) (t :: m) (b :: k) (t :: k).
(a ~> Act b b)
-> w b t -> p b t -> (Act t t ~> b) -> DayAct w p a b
DayAct (a ~> Act c e
f (a ~> Act c e) -> (c ~> a) -> c ~> Act c e
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l) w c d
w p e f
p (b ~> d
r (b ~> d) -> (Act d f ~> b) -> Act d f ~> d
forall (b :: d) (c :: d) (a :: d). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Act d f ~> b
g)
  (Ob a, Ob b) => r
r \\ :: forall (a :: c) (b :: d) r.
((Ob a, Ob b) => r) -> DayAct w p a b -> r
\\ DayAct a ~> Act c e
f w c d
_ p e f
_ Act d f ~> b
g = r
(Ob a, Ob (Act c e)) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (Act c e)) => r) -> (a ~> Act c e) -> r
forall (a :: c) (b :: c) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> Act c e
f ((Ob (Act d f), Ob b) => r) -> (Act d f ~> b) -> r
forall (a :: d) (b :: d) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Act d f ~> b
g

instance (MonoidalAction m c, MonoidalAction m' d) => MonoidalAction (PRO m m') (PRO c d) where
  type Act (w :: PRO m m') (p :: PRO c d) = DayAct w p
  act :: forall (p :: PRO m m') (q :: PRO m m') (x :: PRO c d)
       (y :: PRO c d).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act (Prof p :~> q
n) (Prof x :~> y
m) = (DayAct p x :~> DayAct q y) -> Prof (DayAct p x) (DayAct q y)
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(DayAct a ~> Act c e
f p c d
w x e f
p Act d f ~> b
g) -> (a ~> Act c e)
-> q c d -> y e f -> (Act d f ~> b) -> DayAct q y a b
forall {k} {m} {k} {k} (w :: k -> m -> Type) (p :: k -> k -> Type)
       (a :: k) (b :: k) (b :: k) (t :: m) (b :: k) (t :: k).
(a ~> Act b b)
-> w b t -> p b t -> (Act t t ~> b) -> DayAct w p a b
DayAct a ~> Act c e
f (p c d -> q c d
p :~> q
n p c d
w) (x e f -> y e f
x :~> y
m x e f
p) Act d f ~> b
g
  unitor :: forall (x :: PRO c d). Obj x -> Act Unit x ~> x
unitor Prof{} = (DayAct DayUnit x :~> x) -> Prof (DayAct DayUnit x) x
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(DayAct a ~> Act c e
f (DayUnit c ~> Unit
a Unit ~> d
b) x e f
p Act d f ~> b
g) -> (a ~> e) -> (f ~> b) -> x e f -> x a b
forall (c :: c) (a :: c) (b :: d) (d :: d).
(c ~> a) -> (b ~> d) -> x a b -> x c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall m k (x :: k). MonoidalAction m k => Obj x -> Act Unit x ~> x
unitor @m (x e f -> Obj e
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src x e f
p) (Act Unit e ~> e) -> (a ~> Act Unit e) -> a ~> e
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (c ~> Unit) -> Obj e -> Act c e ~> Act Unit e
forall (p :: m) (q :: m) (x :: c) (y :: c).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act c ~> Unit
a (x e f -> Obj e
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src x e f
p) (Act c e ~> Act Unit e) -> (a ~> Act c e) -> a ~> Act Unit e
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Act c e
f) (Act d f ~> b
g (Act d f ~> b) -> (f ~> Act d f) -> f ~> b
forall (b :: d) (c :: d) (a :: d). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Unit ~> d) -> (f ~> f) -> Act Unit f ~> Act d f
forall (p :: m') (q :: m') (x :: d) (y :: d).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act Unit ~> d
b (x e f -> f ~> f
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt x e f
p) (Act Unit f ~> Act d f) -> (f ~> Act Unit f) -> f ~> Act d f
forall (b :: d) (c :: d) (a :: d). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall m k (x :: k). MonoidalAction m k => Obj x -> x ~> Act Unit x
unitorInv @m' (x e f -> f ~> f
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt x e f
p)) x e f
p ((Ob e, Ob f) => x a b) -> x e f -> x a b
forall (a :: c) (b :: d) r. ((Ob a, Ob b) => r) -> x a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ x e f
p
  unitorInv :: forall (x :: PRO c d). Obj x -> x ~> Act Unit x
unitorInv Prof{} = (x :~> DayAct DayUnit x) -> Prof x (DayAct DayUnit x)
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \x a b
p -> (a ~> Act Unit a)
-> DayUnit Unit Unit
-> x a b
-> (Act Unit b ~> b)
-> DayAct DayUnit x a b
forall {k} {m} {k} {k} (w :: k -> m -> Type) (p :: k -> k -> Type)
       (a :: k) (b :: k) (b :: k) (t :: m) (b :: k) (t :: k).
(a ~> Act b b)
-> w b t -> p b t -> (Act t t ~> b) -> DayAct w p a b
DayAct (forall m k (x :: k). MonoidalAction m k => Obj x -> x ~> Act Unit x
unitorInv @m (x a b -> Obj a
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src x a b
p)) ((Unit ~> Unit) -> (Unit ~> Unit) -> DayUnit Unit Unit
forall {k} {k1} (a :: k) (b :: k1).
(a ~> Unit) -> (Unit ~> b) -> DayUnit a b
DayUnit Unit ~> Unit
forall (a :: m). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id Unit ~> Unit
forall (a :: m'). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) x a b
p (forall m k (x :: k). MonoidalAction m k => Obj x -> Act Unit x ~> x
unitor @m' (x a b -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt x a b
p)) ((Ob a, Ob b) => DayAct DayUnit x a b)
-> x a b -> DayAct DayUnit x a b
forall (a :: c) (b :: d) r. ((Ob a, Ob b) => r) -> x a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ x a b
p
  multiplicator :: forall (p :: PRO m m') (q :: PRO m m') (x :: PRO c d).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator Prof{} Prof{} Prof{} = (DayAct p (DayAct q x) :~> DayAct (Day p q) x)
-> Prof (DayAct p (DayAct q x)) (DayAct (Day p q) x)
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(DayAct a ~> Act c e
f p c d
w (DayAct e ~> Act c e
f' q c d
w' x e f
p Act d f ~> f
g') Act d f ~> b
g) ->
    let c1 :: Obj c
c1 = p c d -> Obj c
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p c d
w; c2 :: Obj c
c2 = q c d -> Obj c
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src q c d
w'; d1 :: Obj d
d1 = p c d -> Obj d
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt p c d
w; d2 :: Obj d
d2 = q c d -> Obj d
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt q c d
w'
    in (a ~> Act (c ** c) e)
-> Day p q (c ** c) (d ** d)
-> x e f
-> (Act (d ** d) f ~> b)
-> DayAct (Day p q) x a b
forall {k} {m} {k} {k} (w :: k -> m -> Type) (p :: k -> k -> Type)
       (a :: k) (b :: k) (b :: k) (t :: m) (b :: k) (t :: k).
(a ~> Act b b)
-> w b t -> p b t -> (Act t t ~> b) -> DayAct w p a b
DayAct
      (Obj c -> Obj c -> Obj e -> Act c (Act c e) ~> Act (c ** c) e
forall (p :: m) (q :: m) (x :: c).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator Obj c
c1 Obj c
c2 (x e f -> Obj e
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src x e f
p) (Act c (Act c e) ~> Act (c ** c) e)
-> (a ~> Act c (Act c e)) -> a ~> Act (c ** c) e
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj c -> (e ~> Act c e) -> Act c e ~> Act c (Act c e)
forall (p :: m) (q :: m) (x :: c) (y :: c).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act Obj c
c1 e ~> Act c e
f' (Act c e ~> Act c (Act c e))
-> (a ~> Act c e) -> a ~> Act c (Act c e)
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Act c e
f)
      (((c ** c) ~> (c ** c))
-> p c d
-> q c d
-> ((d ** d) ~> (d ** d))
-> Day p q (c ** c) (d ** d)
forall {k} {k1} (p :: k -> k1 -> Type) (q :: k -> k1 -> Type)
       (a :: k) (b :: k1) (c :: k) (d :: k1) (e :: k) (f :: k1).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day (c ** c) ~> (c ** c)
forall (a :: m). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id p c d
w q c d
w' (d ** d) ~> (d ** d)
forall (a :: m'). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
      x e f
p
      (Act d f ~> b
g (Act d f ~> b)
-> (Act (d ** d) f ~> Act d f) -> Act (d ** d) f ~> b
forall (b :: d) (c :: d) (a :: d). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj d -> (Act d f ~> f) -> Act d (Act d f) ~> Act d f
forall (p :: m') (q :: m') (x :: d) (y :: d).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act Obj d
d1 Act d f ~> f
g' (Act d (Act d f) ~> Act d f)
-> (Act (d ** d) f ~> Act d (Act d f)) -> Act (d ** d) f ~> Act d f
forall (b :: d) (c :: d) (a :: d). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj d -> Obj d -> Obj f -> Act (d ** d) f ~> Act d (Act d f)
forall (p :: m') (q :: m') (x :: d).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv Obj d
d1 Obj d
d2 (x e f -> Obj f
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt x e f
p))
    ((Ob (c ** c), Ob (c ** c)) => DayAct (Day p q) x a b)
-> ((c ** c) ~> (c ** c)) -> DayAct (Day p q) x a b
forall (a :: m) (b :: m) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj c
c1 Obj c -> Obj c -> (c ** c) ~> (c ** c)
forall (a :: m) (b :: m) (c :: m) (d :: m).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj c
c2) ((Ob (d ** d), Ob (d ** d)) => DayAct (Day p q) x a b)
-> ((d ** d) ~> (d ** d)) -> DayAct (Day p q) x a b
forall (a :: m') (b :: m') r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj d
d1 Obj d -> Obj d -> (d ** d) ~> (d ** d)
forall (a :: m') (b :: m') (c :: m') (d :: m').
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Obj d
d2)
  multiplicatorInv :: forall (p :: PRO m m') (q :: PRO m m') (x :: PRO c d).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv Prof{} Prof{} Prof{} = (DayAct (Day p q) x :~> DayAct p (DayAct q x))
-> Prof (DayAct (Day p q) x) (DayAct p (DayAct q x))
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(DayAct a ~> Act c e
f (Day c ~> (c ** e)
f' p c d
w q e f
w' (d ** f) ~> d
g') x e f
p Act d f ~> b
g) ->
    let c1 :: Obj c
c1 = p c d -> Obj c
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p c d
w; c2 :: Obj e
c2 = q e f -> Obj e
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src q e f
w'; d1 :: Obj d
d1 = p c d -> Obj d
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt p c d
w; d2 :: Obj f
d2 = q e f -> Obj f
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt q e f
w'; e :: Obj e
e = x e f -> Obj e
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src x e f
p; e' :: Obj f
e' = x e f -> Obj f
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt x e f
p
    in (a ~> Act c (Act e e))
-> p c d
-> DayAct q x (Act e e) (Act f f)
-> (Act d (Act f f) ~> b)
-> DayAct p (DayAct q x) a b
forall {k} {m} {k} {k} (w :: k -> m -> Type) (p :: k -> k -> Type)
       (a :: k) (b :: k) (b :: k) (t :: m) (b :: k) (t :: k).
(a ~> Act b b)
-> w b t -> p b t -> (Act t t ~> b) -> DayAct w p a b
DayAct
      (Obj c -> Obj e -> Obj e -> Act (c ** e) e ~> Act c (Act e e)
forall (p :: m) (q :: m) (x :: c).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv Obj c
c1 Obj e
c2 Obj e
e (Act (c ** e) e ~> Act c (Act e e))
-> (a ~> Act (c ** e) e) -> a ~> Act c (Act e e)
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (c ~> (c ** e)) -> Obj e -> Act c e ~> Act (c ** e) e
forall (p :: m) (q :: m) (x :: c) (y :: c).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act c ~> (c ** e)
f' Obj e
e (Act c e ~> Act (c ** e) e)
-> (a ~> Act c e) -> a ~> Act (c ** e) e
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Act c e
f)
      p c d
w
      ((Act e e ~> Act e e)
-> q e f
-> x e f
-> (Act f f ~> Act f f)
-> DayAct q x (Act e e) (Act f f)
forall {k} {m} {k} {k} (w :: k -> m -> Type) (p :: k -> k -> Type)
       (a :: k) (b :: k) (b :: k) (t :: m) (b :: k) (t :: k).
(a ~> Act b b)
-> w b t -> p b t -> (Act t t ~> b) -> DayAct w p a b
DayAct Act e e ~> Act e e
forall (a :: c). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id q e f
w' x e f
p Act f f ~> Act f f
forall (a :: d). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
      (Act d f ~> b
g (Act d f ~> b)
-> (Act d (Act f f) ~> Act d f) -> Act d (Act f f) ~> b
forall (b :: d) (c :: d) (a :: d). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((d ** f) ~> d) -> Obj f -> Act (d ** f) f ~> Act d f
forall (p :: m') (q :: m') (x :: d) (y :: d).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act (d ** f) ~> d
g' Obj f
e' (Act (d ** f) f ~> Act d f)
-> (Act d (Act f f) ~> Act (d ** f) f)
-> Act d (Act f f) ~> Act d f
forall (b :: d) (c :: d) (a :: d). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj d -> Obj f -> Obj f -> Act d (Act f f) ~> Act (d ** f) f
forall (p :: m') (q :: m') (x :: d).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator Obj d
d1 Obj f
d2 Obj f
e')
    ((Ob (Act e e), Ob (Act e e)) => DayAct p (DayAct q x) a b)
-> (Act e e ~> Act e e) -> DayAct p (DayAct q x) a b
forall (a :: c) (b :: c) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj e
c2 Obj e -> Obj e -> Act e e ~> Act e e
forall (p :: m) (q :: m) (x :: c) (y :: c).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
`act` Obj e
e) ((Ob (Act f f), Ob (Act f f)) => DayAct p (DayAct q x) a b)
-> (Act f f ~> Act f f) -> DayAct p (DayAct q x) a b
forall (a :: d) (b :: d) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Obj f
d2 Obj f -> Obj f -> Act f f ~> Act f f
forall (p :: m') (q :: m') (x :: d) (y :: d).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
`act` Obj f
e')


type ModuleObject :: forall {m} {c}. m -> c -> Constraint
class (MonoidalAction m c, Monoid a, Ob n) => ModuleObject (a :: m) (n :: c) where
  action :: Act a n ~> n


class (MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d, Profunctor p) => Tambara (w :: PRO m m') (p :: PRO c d) where
  tambara :: w x x' -> p a b -> p (x `Act` a) (x' `Act` b)

instance (Profunctor p, Tambara w p) => ModuleObject w p where
  action :: Act w p ~> p
action = (DayAct w p :~> p) -> Prof (DayAct w p) p
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(DayAct a ~> Act c e
f w c d
w p e f
p Act d f ~> b
g) -> (a ~> Act c e) -> (Act d f ~> b) -> p (Act c e) (Act d f) -> p a b
forall (c :: c) (a :: c) (b :: d) (d :: d).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> Act c e
f Act d f ~> b
g (p (Act c e) (Act d f) -> p a b) -> p (Act c e) (Act d f) -> p a b
forall a b. (a -> b) -> a -> b
$ w c d -> p e f -> p (Act c e) (Act d f)
forall (x :: m) (x' :: m') (a :: c) (b :: d).
w x x' -> p a b -> p (Act x a) (Act x' b)
forall m m' c d (w :: PRO m m') (p :: PRO c d) (x :: m) (x' :: m')
       (a :: c) (b :: d).
Tambara w p =>
w x x' -> p a b -> p (Act x a) (Act x' b)
tambara w c d
w p e f
p

data Optic w a b s t where
  Optic :: forall {c} {d} a b s t m m' w (x :: m) (x' :: m')
        . (Ob (a :: c), Ob (b :: d))
        => s ~> (x `Act` a)
        -> w x x'
        -> (x' `Act` b) ~> t
        -> Optic (w :: PRO m m') a b s t

opticAsDayAct :: (CategoryOf c, CategoryOf d) => Optic w (a :: c) (b :: d) :~> DayAct w (Yo a b)
opticAsDayAct :: forall {k} {m} c d (w :: PRO k m) (a :: c) (b :: d).
(CategoryOf c, CategoryOf d) =>
Optic w a b :~> DayAct w (Yo a b)
opticAsDayAct (Optic a ~> Act x a
f w x x'
w Act x' b ~> b
g) = (a ~> Act x a)
-> w x x' -> Yo a b a b -> (Act x' b ~> b) -> DayAct w (Yo a b) a b
forall {k} {m} {k} {k} (w :: k -> m -> Type) (p :: k -> k -> Type)
       (a :: k) (b :: k) (b :: k) (t :: m) (b :: k) (t :: k).
(a ~> Act b b)
-> w b t -> p b t -> (Act t t ~> b) -> DayAct w p a b
DayAct a ~> Act x a
f w x x'
w ((a ~> a) -> (b ~> b) -> Yo a b a b
forall {k} {k1} (a :: k) (b :: k1) (c :: k) (d :: k1).
(c ~> a) -> (b ~> d) -> Yo a b c d
Yo a ~> a
forall (a :: c). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: d). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) Act x' b ~> b
g

dayActAsOptic
  :: (MonoidalAction m c, MonoidalAction m' d, Profunctor (w :: PRO m m'))
  => DayAct w (Yo (a :: c) (b :: d)) :~> Optic w a b
dayActAsOptic :: forall m c m' d (w :: PRO m m') (a :: c) (b :: d).
(MonoidalAction m c, MonoidalAction m' d, Profunctor w) =>
DayAct w (Yo a b) :~> Optic w a b
dayActAsOptic (DayAct a ~> Act c e
f w c d
w (Yo e ~> a
l b ~> f
r) Act d f ~> b
g) = (a ~> Act c a) -> w c d -> (Act d b ~> b) -> Optic w a b a b
forall {c} {d} (a :: c) (b :: d) (s :: c) (t :: d) m m'
       (w :: PRO m m') (b :: m) (t :: m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic ((c ~> c) -> (e ~> a) -> Act c e ~> Act c a
forall (p :: m) (q :: m) (x :: c) (y :: c).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act (w c d -> c ~> c
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src w c d
w) e ~> a
l (Act c e ~> Act c a) -> (a ~> Act c e) -> a ~> Act c a
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Act c e
f) w c d
w (Act d f ~> b
g (Act d f ~> b) -> (Act d b ~> Act d f) -> Act d b ~> b
forall (b :: d) (c :: d) (a :: d). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (d ~> d) -> (b ~> f) -> Act d b ~> Act d f
forall (p :: m') (q :: m') (x :: d) (y :: d).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act (w c d -> d ~> d
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt w c d
w) b ~> f
r) ((Ob e, Ob a) => Optic w a b a b) -> (e ~> a) -> Optic w a b a b
forall (a :: c) (b :: c) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ e ~> a
l ((Ob b, Ob f) => Optic w a b a b) -> (b ~> f) -> Optic w a b a b
forall (a :: d) (b :: d) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> f
r

instance (CategoryOf c, CategoryOf d) => Profunctor (Optic w (a :: c) (b :: d)) where
  dimap :: forall (c :: c) (a :: c) (b :: d) (d :: d).
(c ~> a) -> (b ~> d) -> Optic w a b a b -> Optic w a b c d
dimap c ~> a
l b ~> d
r (Optic a ~> Act x a
f w x x'
w Act x' b ~> b
g) = (c ~> Act x a) -> w x x' -> (Act x' b ~> d) -> Optic w a b c d
forall {c} {d} (a :: c) (b :: d) (s :: c) (t :: d) m m'
       (w :: PRO m m') (b :: m) (t :: m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic (a ~> Act x a
f (a ~> Act x a) -> (c ~> a) -> c ~> Act x a
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
l) w x x'
w (b ~> d
r (b ~> d) -> (Act x' b ~> b) -> Act x' b ~> d
forall (b :: d) (c :: d) (a :: d). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Act x' b ~> b
g)
  (Ob a, Ob b) => r
r \\ :: forall (a :: c) (b :: d) r.
((Ob a, Ob b) => r) -> Optic w a b a b -> r
\\ Optic a ~> Act x a
f w x x'
_ Act x' b ~> b
g = r
(Ob a, Ob (Act x a)) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (Act x a)) => r) -> (a ~> Act x a) -> r
forall (a :: c) (b :: c) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> Act x a
f ((Ob (Act x' b), Ob b) => r) -> (Act x' b ~> b) -> r
forall (a :: d) (b :: d) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Act x' b ~> b
g

instance (MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d) => Tambara (w :: PRO m m') (Optic w (a :: c) (b :: d)) where
  tambara :: forall (x :: m) (x' :: m') (a :: c) (b :: d).
w x x' -> Optic w a b a b -> Optic w a b (Act x a) (Act x' b)
tambara w x x'
w (Optic a ~> Act x a
f w x x'
w' Act x' b ~> b
g) = (Act x a ~> Act (x ** x) a)
-> w (x ** x) (x' ** x')
-> (Act (x' ** x') b ~> Act x' b)
-> Optic w a b (Act x a) (Act x' b)
forall {c} {d} (a :: c) (b :: d) (s :: c) (t :: d) m m'
       (w :: PRO m m') (b :: m) (t :: m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic
    (Obj x -> Obj x -> Obj a -> Act x (Act x a) ~> Act (x ** x) a
forall (p :: m) (q :: m) (x :: c).
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act p (Act q x) ~> Act (p ** q) x
multiplicator (w x x' -> Obj x
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src w x x'
w) (w x x' -> Obj x
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src w x x'
w') (forall (a :: c). (CategoryOf c, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (Act x (Act x a) ~> Act (x ** x) a)
-> (Act x a ~> Act x (Act x a)) -> Act x a ~> Act (x ** x) a
forall (b :: c) (c :: c) (a :: c). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj x -> (a ~> Act x a) -> Act x a ~> Act x (Act x a)
forall (p :: m) (q :: m) (x :: c) (y :: c).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act (w x x' -> Obj x
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src w x x'
w) a ~> Act x a
f)
    (w x x' -> w x x' -> w (x ** x) (x' ** x')
forall (x1 :: m) (x2 :: m') (y1 :: m) (y2 :: m').
w x1 x2 -> w y1 y2 -> w (x1 ** y1) (x2 ** y2)
forall j k (p :: PRO j k) (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
lift2 w x x'
w w x x'
w')
    ((x' ~> x') -> (Act x' b ~> b) -> Act x' (Act x' b) ~> Act x' b
forall (p :: m') (q :: m') (x :: d) (y :: d).
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
forall m k (p :: m) (q :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(p ~> q) -> (x ~> y) -> Act p x ~> Act q y
act (w x x' -> x' ~> x'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt w x x'
w) Act x' b ~> b
g (Act x' (Act x' b) ~> Act x' b)
-> (Act (x' ** x') b ~> Act x' (Act x' b))
-> Act (x' ** x') b ~> Act x' b
forall (b :: d) (c :: d) (a :: d). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x' ~> x')
-> Obj x' -> Obj b -> Act (x' ** x') b ~> Act x' (Act x' b)
forall (p :: m') (q :: m') (x :: d).
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
forall m k (p :: m) (q :: m) (x :: k).
MonoidalAction m k =>
Obj p -> Obj q -> Obj x -> Act (p ** q) x ~> Act p (Act q x)
multiplicatorInv (w x x' -> x' ~> x'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt w x x'
w) (w x x' -> Obj x'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt w x x'
w') (forall (a :: d). (CategoryOf d, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b))

parallel :: Optic w a b s t -> Optic w' c d u v -> Optic (w :**: w') '(a, c) '(b, d) '(s, u) '(t, v)
parallel :: forall {k1} {k} {k} {k2} {k} {k} (w :: PRO k1 k1) (a :: k) (b :: k)
       (s :: k) (t :: k) (w' :: PRO k2 k2) (c :: k) (d :: k) (u :: k)
       (v :: k).
Optic w a b s t
-> Optic w' c d u v
-> Optic (w :**: w') '(a, c) '(b, d) '(s, u) '(t, v)
parallel (Optic s ~> Act x a
f w x x'
w Act x' b ~> t
g) (Optic u ~> Act x c
h w' x x'
w' Act x' d ~> v
i) = ('(s, u) ~> Act '(x, x) '(a, c))
-> (:**:) w w' '(x, x) '(x', x')
-> (Act '(x', x') '(b, d) ~> '(t, v))
-> Optic (w :**: w') '(a, c) '(b, d) '(s, u) '(t, v)
forall {c} {d} (a :: c) (b :: d) (s :: c) (t :: d) m m'
       (w :: PRO m m') (b :: m) (t :: m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic (s ~> Act x a
f (s ~> Act x a)
-> (u ~> Act x c) -> (:**:) (~>) (~>) '(s, u) '(Act x a, Act x c)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: u ~> Act x c
h) (w x x'
w w x x' -> w' x x' -> (:**:) w w' '(x, x) '(x', x')
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: w' x x'
w') (Act x' b ~> t
g (Act x' b ~> t)
-> (Act x' d ~> v)
-> (:**:) (~>) (~>) '(Act x' b, Act x' d) '(t, v)
forall {k1} {k2} (c :: CAT k1) (a1 :: k1) (b1 :: k1) (d :: CAT k2)
       (a2 :: k2) (b2 :: k2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Act x' d ~> v
i)


type data OPTIC (w :: PRO m m') (c :: Kind) (d :: Kind) = OPT c d
type family LCat (p :: OPTIC w c d) where LCat (OPT c d) = c
type family RCat (p :: OPTIC w c d) where RCat (OPT c d) = d
type OpticCat :: CAT (OPTIC w c d)
data OpticCat ab st where
  OpticCat :: Optic w a b s t -> OpticCat (OPT a b :: OPTIC w c d) (OPT s t)

instance (MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d) => Profunctor (OpticCat :: CAT (OPTIC (w :: PRO m m') c d)) where
  dimap :: forall (c :: OPTIC w c d) (a :: OPTIC w c d) (b :: OPTIC w c d)
       (d :: OPTIC w c d).
(c ~> a) -> (b ~> d) -> OpticCat a b -> OpticCat c d
dimap = (c ~> a) -> (b ~> d) -> OpticCat a b -> OpticCat c d
OpticCat c a -> OpticCat b d -> OpticCat a b -> OpticCat c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: OPTIC w c d) (b :: OPTIC w c d) r.
((Ob a, Ob b) => r) -> OpticCat a b -> r
\\ OpticCat (Optic s ~> Act x a
f w x x'
_ Act x' b ~> t
g) = r
(Ob s, Ob (Act x a)) => r
(Ob a, Ob b) => r
r ((Ob s, Ob (Act x a)) => r) -> (s ~> Act x a) -> r
forall (a :: c) (b :: c) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ s ~> Act x a
f ((Ob (Act x' b), Ob t) => r) -> (Act x' b ~> t) -> r
forall (a :: d) (b :: d) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Act x' b ~> t
g
instance (MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d) => Promonad (OpticCat :: CAT (OPTIC (w :: PRO m m') c d)) where
  id :: forall (a :: OPTIC w c d). Ob a => OpticCat a a
id = Optic w (LCat a) (RCat a) (LCat a) (RCat a)
-> OpticCat (OPT (LCat a) (RCat a)) (OPT (LCat a) (RCat a))
forall {m} {m'} (w :: PRO m m') c (b :: c) d (t :: d) (b :: c)
       (t :: d).
Optic w b t b t -> OpticCat (OPT b t) (OPT b t)
OpticCat (ProfOptic w (LCat a) (RCat a) (LCat a) (RCat a)
-> Optic w (LCat a) (RCat a) (LCat a) (RCat a)
forall {c} {d} m m' (w :: PRO m m') (a :: c) (b :: d) (s :: c)
       (t :: d).
(MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d,
 Ob a, Ob b) =>
ProfOptic w a b s t -> Optic w a b s t
prof2ex p (LCat a) (RCat a) -> p (LCat a) (RCat a)
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
ProfOptic w (LCat a) (RCat a) (LCat a) (RCat a)
id)
  OpticCat l :: Optic w a b s t
l@Optic{} . :: forall (b :: OPTIC w c d) (c :: OPTIC w c d) (a :: OPTIC w c d).
OpticCat b c -> OpticCat a b -> OpticCat a c
. OpticCat r :: Optic w a b s t
r@Optic{} = Optic w a b s t -> OpticCat (OPT a b) (OPT s t)
forall {m} {m'} (w :: PRO m m') c (b :: c) d (t :: d) (b :: c)
       (t :: d).
Optic w b t b t -> OpticCat (OPT b t) (OPT b t)
OpticCat (Optic w a b s t -> OpticCat (OPT a b) (OPT s t))
-> Optic w a b s t -> OpticCat (OPT a b) (OPT s t)
forall a b. (a -> b) -> a -> b
$ ProfOptic w a b s t -> Optic w a b s t
forall {c} {d} m m' (w :: PRO m m') (a :: c) (b :: d) (s :: c)
       (t :: d).
(MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d,
 Ob a, Ob b) =>
ProfOptic w a b s t -> Optic w a b s t
prof2ex (Optic w a b s t -> ProfOptic w a b s t
forall {m} {m'} {k} {k} (w :: PRO m m') (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
ex2prof Optic w a b s t
l (p a b -> p s t) -> (p a b -> p a b) -> p a b -> p s t
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Optic w a b s t -> ProfOptic w a b s t
forall {m} {m'} {k} {k} (w :: PRO m m') (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
ex2prof Optic w a b s t
r)
instance (MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d) => CategoryOf (OPTIC (w :: PRO m m') c d) where
  type (~>) = OpticCat
  type Ob a = (a ~ OPT (LCat a) (RCat a), Ob (LCat a), Ob (RCat a))


type ProfOptic w a b s t = forall p. Tambara w p => p a b -> p s t
type MixedOptic m a b s t = ProfOptic ((~>) @m) a b s t

ex2prof :: Optic w a b s t -> ProfOptic w a b s t
ex2prof :: forall {m} {m'} {k} {k} (w :: PRO m m') (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
ex2prof (Optic s ~> Act x a
l w x x'
w Act x' b ~> t
r) = (s ~> Act x a)
-> (Act x' b ~> t) -> p (Act x a) (Act x' b) -> p s t
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap s ~> Act x a
l Act x' b ~> t
r (p (Act x a) (Act x' b) -> p s t)
-> (p a b -> p (Act x a) (Act x' b)) -> p a b -> p s t
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. w x x' -> p a b -> p (Act x a) (Act x' b)
forall (x :: m) (x' :: m') (a :: k) (b :: k).
w x x' -> p a b -> p (Act x a) (Act x' b)
forall m m' c d (w :: PRO m m') (p :: PRO c d) (x :: m) (x' :: m')
       (a :: c) (b :: d).
Tambara w p =>
w x x' -> p a b -> p (Act x a) (Act x' b)
tambara w x x'
w

prof2ex
  :: forall {c} {d} m m' w a b s t
   . (MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d, Ob a, Ob b)
   => ProfOptic (w :: PRO m m') (a :: c) (b :: d) (s :: c) (t :: d)
   -> Optic w a b s t
prof2ex :: forall {c} {d} m m' (w :: PRO m m') (a :: c) (b :: d) (s :: c)
       (t :: d).
(MonoidalProfunctor w, MonoidalAction m c, MonoidalAction m' d,
 Ob a, Ob b) =>
ProfOptic w a b s t -> Optic w a b s t
prof2ex ProfOptic w a b s t
p2p = Optic w a b a b -> Optic w a b s t
ProfOptic w a b s t
p2p ((a ~> Act Unit a)
-> w Unit Unit -> (Act Unit b ~> b) -> Optic w a b a b
forall {c} {d} (a :: c) (b :: d) (s :: c) (t :: d) m m'
       (w :: PRO m m') (b :: m) (t :: m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic (forall m k (x :: k). MonoidalAction m k => Obj x -> x ~> Act Unit x
unitorInv @m Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj) w Unit Unit
forall j k (p :: PRO j k). MonoidalProfunctor p => p Unit Unit
lift0 (forall m k (x :: k). MonoidalAction m k => Obj x -> Act Unit x ~> x
unitor @m' Obj b
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj))



type Lens s t a b = MixedOptic Type a b s t
mkLens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
mkLens :: forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
mkLens s -> a
sa s -> b -> t
sbt = Optic (~>) a b s t -> ProfOptic (~>) a b s t
forall {m} {m'} {k} {k} (w :: PRO m m') (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
ex2prof ((s ~> Act s a) -> (s ~> s) -> (Act s b ~> t) -> Optic (~>) a b s t
forall {c} {d} (a :: c) (b :: d) (s :: c) (t :: d) m m'
       (w :: PRO m m') (b :: m) (t :: m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic (\s
s -> (s
s, s -> a
sa s
s)) ((s -> a) -> s ~> s
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src s -> a
sa) ((s -> b -> t) -> (s, b) -> t
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry s -> b -> t
sbt))

type Prism s t a b = MixedOptic (COPROD Type) (COPR a) (COPR b) (COPR s) (COPR t)
mkPrism :: (s -> Either t a) -> (b -> t) -> Prism s t a b
mkPrism :: forall s t a b. (s -> Either t a) -> (b -> t) -> Prism s t a b
mkPrism s -> Either t a
sat b -> t
bt = Optic Coprod ('COPR a) ('COPR b) ('COPR s) ('COPR t)
-> ProfOptic Coprod ('COPR a) ('COPR b) ('COPR s) ('COPR t)
forall {m} {m'} {k} {k} (w :: PRO m m') (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
ex2prof (('COPR s ~> Act ('COPR t) ('COPR a))
-> Coprod ('COPR t) ('COPR t)
-> (Act ('COPR t) ('COPR b) ~> 'COPR t)
-> Optic Coprod ('COPR a) ('COPR b) ('COPR s) ('COPR t)
forall {c} {d} (a :: c) (b :: d) (s :: c) (t :: d) m m'
       (w :: PRO m m') (b :: m) (t :: m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic ((UN 'COPR ('COPR s) ~> UN 'COPR (Act ('COPR t) ('COPR a)))
-> Coprod ('COPR s) (Act ('COPR t) ('COPR a))
forall {k} (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(UN 'COPR a ~> UN 'COPR b) -> Coprod a b
Coprod UN 'COPR ('COPR s) ~> UN 'COPR (Act ('COPR t) ('COPR a))
s -> Either t a
sat) ((UN 'COPR ('COPR t) ~> UN 'COPR ('COPR t))
-> Coprod ('COPR t) ('COPR t)
forall {k} (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(UN 'COPR a ~> UN 'COPR b) -> Coprod a b
Coprod ((b -> UN 'COPR ('COPR t))
-> UN 'COPR ('COPR t) ~> UN 'COPR ('COPR t)
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt b -> t
b -> UN 'COPR ('COPR t)
bt)) ((UN 'COPR ('COPR (Either t b)) ~> UN 'COPR ('COPR t))
-> Coprod ('COPR (Either t b)) ('COPR t)
forall {k} (a :: COPROD k) (b :: COPROD k).
(Ob a, Ob b) =>
(UN 'COPR a ~> UN 'COPR b) -> Coprod a b
Coprod ((t -> t) -> (b -> t) -> Either t b -> t
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either t -> t
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id b -> t
bt)))

type Traversal s t a b = MixedOptic (Type -> Type) a b s t
traversing :: Traversable f => Traversal (f a) (f b) a b
traversing :: forall (f :: Type -> Type) a b.
Traversable f =>
Traversal (f a) (f b) a b
traversing = forall {m} {m'} {k} {k} (w :: PRO m m') (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
forall (w :: PRO (Type -> Type) (Type -> Type)) a b s t.
Optic w a b s t -> ProfOptic w a b s t
ex2prof @((~>) @(Type -> Type)) ((f a ~> Act (Prelude f) a)
-> Nat (Prelude f) (Prelude f)
-> (Act (Prelude f) b ~> f b)
-> Optic Nat a b (f a) (f b)
forall {c} {d} (a :: c) (b :: d) (s :: c) (t :: d) m m'
       (w :: PRO m m') (b :: m) (t :: m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic f a ~> Act (Prelude f) a
f a -> Prelude f a
forall {k} (f :: k -> Type) (a :: k). f a -> Prelude f a
Prelude Nat (Prelude f) (Prelude f)
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Type -> Type). Ob a => Nat a a
id Act (Prelude f) b ~> f b
Prelude f b -> f b
forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
getPrelude)

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

type AlgebraicLens m s t a b = MixedOptic (SUBCAT (Algebra m)) a b s t
mkAlgebraicLens :: forall m s t a b. Monad m => (s -> a) -> (m s -> b -> t) -> AlgebraicLens m s t a b
mkAlgebraicLens :: forall (m :: Type -> Type) s t a b.
Monad m =>
(s -> a) -> (m s -> b -> t) -> AlgebraicLens m s t a b
mkAlgebraicLens s -> a
v m s -> b -> t
u = forall {m} {m'} {k} {k} (w :: PRO m m') (a :: k) (b :: k) (s :: k)
       (t :: k).
Optic w a b s t -> ProfOptic w a b s t
forall (w :: PRO (SUBCAT (Algebra m)) (SUBCAT (Algebra m))) a b s
       t.
Optic w a b s t -> ProfOptic w a b s t
ex2prof @((~>) @(SUBCAT (Algebra m))) ((s ~> Act (SUB (m s)) a)
-> Sub (SUB (m s)) (SUB (m s))
-> (Act (SUB (m s)) b ~> t)
-> Optic Sub a b s t
forall {c} {d} (a :: c) (b :: d) (s :: c) (t :: d) m m'
       (w :: PRO m m') (b :: m) (t :: m').
(Ob a, Ob b) =>
(s ~> Act b a) -> w b t -> (Act t b ~> t) -> Optic w a b s t
Optic (\s
s -> (forall (m :: Type -> Type) a. Monad m => a -> m a
return @m s
s, s -> a
v s
s)) ((m s ~> m s) -> Sub (SUB (m s)) (SUB (m s))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k).
(ob a1, ob b1) =>
(a1 ~> b1) -> Sub (SUB a1) (SUB b1)
Sub m s ~> m s
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj) ((m s -> b -> t) -> (m s, b) -> t
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry m s -> b -> t
u))



newtype Viewing a (b :: Type) s (t :: Type) = Viewing { forall a b s t. Viewing a b s t -> s -> a
getView :: s -> a }
instance Profunctor (Viewing a b) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> Viewing a b a b -> Viewing a b c d
dimap c ~> a
l b ~> d
_ (Viewing a -> a
f) = (c -> a) -> Viewing a b c d
forall a b s t. (s -> a) -> Viewing a b s t
Viewing (a -> a
f (a -> a) -> (c -> a) -> c -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
c -> a
l)
instance Tambara (->) (Viewing a b) where
  tambara :: forall x x' a b.
(x -> x') -> Viewing a b a b -> Viewing a b (Act x a) (Act x' b)
tambara x -> x'
_ (Viewing a -> a
f) = ((x, a) -> a) -> Viewing a b (x, a) (x', b)
forall a b s t. (s -> a) -> Viewing a b s t
Viewing (a -> a
f (a -> a) -> ((x, a) -> a) -> (x, a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x, a) -> a
forall a b. (a, b) -> b
snd)

infixl 8 ^.
(^.) :: s -> (Viewing a b a b -> Viewing a b s t) -> a
^. :: forall s a b t. s -> (Viewing a b a b -> Viewing a b s t) -> a
(^.) s
s Viewing a b a b -> Viewing a b s t
l = Viewing a b s t -> s -> a
forall a b s t. Viewing a b s t -> s -> a
getView (Viewing a b a b -> Viewing a b s t
l (Viewing a b a b -> Viewing a b s t)
-> Viewing a b a b -> Viewing a b s t
forall a b. (a -> b) -> a -> b
$ (a -> a) -> Viewing a b a b
forall a b s t. (s -> a) -> Viewing a b s t
Viewing a -> a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) s
s


data Previewing a (b :: COPROD Type) s (t :: COPROD Type) where
  Previewing :: { forall b t b t.
Previewing ('COPR t) ('COPR b) ('COPR b) ('COPR t) -> b -> Maybe t
getPreview :: s -> Maybe a } -> Previewing (COPR a) (COPR b) (COPR s) (COPR t)
instance Profunctor (Previewing a b) where
  dimap :: forall (c :: COPROD Type) (a :: COPROD Type) (b :: COPROD Type)
       (d :: COPROD Type).
(c ~> a) -> (b ~> d) -> Previewing a b a b -> Previewing a b c d
dimap (Coprod UN 'COPR c ~> UN 'COPR a
l) Coprod{} (Previewing s -> Maybe a
f) = (UN 'COPR c -> Maybe a)
-> Previewing
     ('COPR a) ('COPR b) ('COPR (UN 'COPR c)) ('COPR (UN 'COPR d))
forall b t b t.
(b -> Maybe t)
-> Previewing ('COPR t) ('COPR b) ('COPR b) ('COPR t)
Previewing (s -> Maybe a
UN 'COPR a -> Maybe a
f (UN 'COPR a -> Maybe a)
-> (UN 'COPR c -> UN 'COPR a) -> UN 'COPR c -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. UN 'COPR c ~> UN 'COPR a
UN 'COPR c -> UN 'COPR a
l)
  (Ob a, Ob b) => r
r \\ :: forall (a :: COPROD Type) (b :: COPROD Type) r.
((Ob a, Ob b) => r) -> Previewing a b a b -> r
\\ Previewing s -> Maybe a
f = r
(Ob s, Ob (Maybe a)) => r
(Ob a, Ob b) => r
r ((Ob s, Ob (Maybe a)) => r) -> (s -> Maybe a) -> r
forall a b r. ((Ob a, Ob b) => r) -> (a -> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ s -> Maybe a
f
instance Tambara (Coprod :: CAT (COPROD Type)) (Previewing a b) where
  tambara :: forall (x :: COPROD Type) (x' :: COPROD Type) (a :: COPROD Type)
       (b :: COPROD Type).
Coprod x x'
-> Previewing a b a b -> Previewing a b (Act x a) (Act x' b)
tambara Coprod{} (Previewing s -> Maybe a
f) = (Either (UN 'COPR x) s -> Maybe a)
-> Previewing
     ('COPR a)
     ('COPR b)
     ('COPR (Either (UN 'COPR x) s))
     ('COPR (Either (UN 'COPR x') t))
forall b t b t.
(b -> Maybe t)
-> Previewing ('COPR t) ('COPR b) ('COPR b) ('COPR t)
Previewing ((UN 'COPR x -> Maybe a)
-> (s -> Maybe a) -> Either (UN 'COPR x) s -> Maybe a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe a -> UN 'COPR x -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing) s -> Maybe a
f)
instance Tambara (->) (Previewing a b) where
  tambara :: forall x x' (a :: COPROD Type) (b :: COPROD Type).
(x -> x')
-> Previewing a b a b -> Previewing a b (Act x a) (Act x' b)
tambara x -> x'
_ (Previewing s -> Maybe a
f) = ((x, s) -> Maybe a)
-> Previewing ('COPR a) ('COPR b) ('COPR (x, s)) ('COPR (x', t))
forall b t b t.
(b -> Maybe t)
-> Previewing ('COPR t) ('COPR b) ('COPR b) ('COPR t)
Previewing (s -> Maybe a
f (s -> Maybe a) -> ((x, s) -> s) -> (x, s) -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x, s) -> s
forall a b. (a, b) -> b
snd)

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


newtype Setting a b s t = Setting { forall a b s t. Setting a b s t -> (a -> b) -> s -> t
getSet :: (a -> b) -> (s -> t) }
instance Profunctor (Setting a b) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> Setting a b a b -> Setting a b c d
dimap c ~> a
l b ~> d
r (Setting (a -> b) -> a -> b
f) = ((a -> b) -> c -> d) -> Setting a b c d
forall a b s t. ((a -> b) -> s -> t) -> Setting a b s t
Setting (\a -> b
u -> b ~> d
b -> d
r (b -> d) -> (c -> b) -> c -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a -> b) -> a -> b
f a -> b
u (a -> b) -> (c -> a) -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
c -> a
l)
instance Tambara (->) (Setting a b) where
  tambara :: forall x x' a b.
(x -> x') -> Setting a b a b -> Setting a b (Act x a) (Act x' b)
tambara x -> x'
w (Setting (a -> b) -> a -> b
f) = ((a -> b) -> (x, a) -> (x', b)) -> Setting a b (x, a) (x', b)
forall a b s t. ((a -> b) -> s -> t) -> Setting a b s t
Setting (\a -> b
u (x
x, a
a) -> (x -> x'
w x
x, (a -> b) -> a -> b
f a -> b
u a
a))
instance Tambara (Coprod :: CAT (COPROD Type)) (Setting a b) where
  tambara :: forall (x :: COPROD Type) (x' :: COPROD Type) a b.
Coprod x x' -> Setting a b a b -> Setting a b (Act x a) (Act x' b)
tambara (Coprod UN 'COPR x ~> UN 'COPR x'
w) (Setting (a -> b) -> a -> b
f) = ((a -> b) -> Either (UN 'COPR x) a -> Either (UN 'COPR x') b)
-> Setting a b (Either (UN 'COPR x) a) (Either (UN 'COPR x') b)
forall a b s t. ((a -> b) -> s -> t) -> Setting a b s t
Setting ((UN 'COPR x -> UN 'COPR x')
-> (a -> b) -> Either (UN 'COPR x) a -> Either (UN 'COPR x') b
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap UN 'COPR x ~> UN 'COPR x'
UN 'COPR x -> UN 'COPR x'
w ((a -> b) -> Either (UN 'COPR x) a -> Either (UN 'COPR x') b)
-> ((a -> b) -> a -> b)
-> (a -> b)
-> Either (UN 'COPR x) a
-> Either (UN 'COPR x') b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a -> b) -> a -> b
f)

infixl 8 .~
(.~) :: (Setting a b a b -> Setting a b s t) -> b -> s -> t
.~ :: forall a b s t. (Setting a b a b -> Setting a b s t) -> b -> s -> t
(.~) Setting a b a b -> Setting a b s t
l b
b = Setting a b s t -> (a -> b) -> s -> t
forall a b s t. Setting a b s t -> (a -> b) -> s -> t
getSet (Setting a b a b -> Setting a b s t
l (Setting a b a b -> Setting a b s t)
-> Setting a b a b -> Setting a b s t
forall a b. (a -> b) -> a -> b
$ ((a -> b) -> a -> b) -> Setting a b a b
forall a b s t. ((a -> b) -> s -> t) -> Setting a b s t
Setting (a -> b) -> a -> b
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id) (b -> a -> b
forall a b. a -> b -> a
const b
b)


type KlCat m = KLEISLI (Star (Prelude m))
data Updating a b s t where
  Update :: { forall {k} b s (m :: Type -> Type) t (a :: k).
Updating a ('KL b) s ('KL t) -> b -> s -> m t
getUpdate :: b -> s -> m t } -> Updating a (KL b :: KlCat m) s (KL t :: KlCat m)
instance Monad m => Profunctor (Updating a b :: PRO Type (KlCat m)) where
  dimap :: forall c a (b :: KlCat m) (d :: KlCat m).
(c ~> a) -> (b ~> d) -> Updating a b a b -> Updating a b c d
dimap c ~> a
l (Kleisli (Star a1 ~> Prelude m b1
r)) (Update b -> a -> m t
u) = (b -> c -> m b1) -> Updating a ('KL b) c ('KL b1)
forall {k} b s (m :: Type -> Type) t (a :: k).
(b -> s -> m t) -> Updating a ('KL b) s ('KL t)
Update (\b
b c
x -> b -> a -> m t
u b
b (c ~> a
c -> a
l c
x) m t -> (t -> m b1) -> m b1
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Prelude m b1 -> m b1
forall {k} (f :: k -> Type) (a :: k). Prelude f a -> f a
getPrelude (Prelude m b1 -> m b1) -> (a1 -> Prelude m b1) -> a1 -> m b1
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a1 ~> Prelude m b1
a1 -> Prelude m b1
r)
  (Ob a, Ob b) => r
r \\ :: forall a (b :: KlCat m) r.
((Ob a, Ob b) => r) -> Updating a b a b -> r
\\ Update b -> a -> m t
u = r
(Ob a, Ob b) => r
(Ob b, Ob (a -> m t)) => r
r ((Ob b, Ob (a -> m t)) => r) -> (b -> a -> m t) -> r
forall a b r. ((Ob a, Ob b) => r) -> (a -> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b -> a -> m t
u
instance Monad m => Tambara (->) (Updating a b :: PRO Type (KlCat m)) where
  tambara :: forall x x' a (b :: KlCat m).
(x -> x') -> Updating a b a b -> Updating a b (Act x a) (Act x' b)
tambara x -> x'
f (Update b -> a -> m t
u) = (b -> (x, a) -> m (x', t))
-> Updating a ('KL b) (x, a) ('KL (x', t))
forall {k} b s (m :: Type -> Type) t (a :: k).
(b -> s -> m t) -> Updating a ('KL b) s ('KL t)
Update (\b
b (x
w, a
x) -> (t -> (x', t)) -> m t -> m (x', t)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (x -> x'
f x
w,) (b -> a -> m t
u b
b a
x))

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


newtype Replacing a b s t = Replace { forall a b s t. Replacing a b s t -> (a -> b) -> s -> t
getReplace :: (a -> b) -> (s -> t) }
instance Profunctor (Replacing a b) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> Replacing a b a b -> Replacing a b c d
dimap c ~> a
l b ~> d
r (Replace (a -> b) -> a -> b
f) = ((a -> b) -> c -> d) -> Replacing a b c d
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace (\a -> b
ab -> b ~> d
b -> d
r (b -> d) -> (c -> b) -> c -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a -> b) -> a -> b
f a -> b
ab (a -> b) -> (c -> a) -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. c ~> a
c -> a
l)
instance Tambara (->) (Replacing a b) where
  tambara :: forall x x' a b.
(x -> x')
-> Replacing a b a b -> Replacing a b (Act x a) (Act x' b)
tambara x -> x'
w (Replace (a -> b) -> a -> b
f) = ((a -> b) -> (x, a) -> (x', b)) -> Replacing a b (x, a) (x', b)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace ((x -> x') -> (a -> b) -> (x, a) -> (x', b)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap x -> x'
w ((a -> b) -> (x, a) -> (x', b))
-> ((a -> b) -> a -> b) -> (a -> b) -> (x, a) -> (x', b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a -> b) -> a -> b
f)
instance Tambara (Coprod :: CAT (COPROD Type)) (Replacing a b) where
  tambara :: forall (x :: COPROD Type) (x' :: COPROD Type) a b.
Coprod x x'
-> Replacing a b a b -> Replacing a b (Act x a) (Act x' b)
tambara (Coprod UN 'COPR x ~> UN 'COPR x'
w) (Replace (a -> b) -> a -> b
f) = ((a -> b) -> Either (UN 'COPR x) a -> Either (UN 'COPR x') b)
-> Replacing a b (Either (UN 'COPR x) a) (Either (UN 'COPR x') b)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace ((UN 'COPR x -> UN 'COPR x')
-> (a -> b) -> Either (UN 'COPR x) a -> Either (UN 'COPR x') b
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap UN 'COPR x ~> UN 'COPR x'
UN 'COPR x -> UN 'COPR x'
w ((a -> b) -> Either (UN 'COPR x) a -> Either (UN 'COPR x') b)
-> ((a -> b) -> a -> b)
-> (a -> b)
-> Either (UN 'COPR x) a
-> Either (UN 'COPR x') b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a -> b) -> a -> b
f)
instance Tambara (Nat :: CAT (Type -> Type)) (Replacing a b) where
  tambara :: forall (x :: Type -> Type) (x' :: Type -> Type) a b.
Nat x x' -> Replacing a b a b -> Replacing a b (Act x a) (Act x' b)
tambara (Nat x .~> x'
w) (Replace (a -> b) -> a -> b
f) = ((a -> b) -> x a -> x' b) -> Replacing a b (x a) (x' b)
forall a b s t. ((a -> b) -> s -> t) -> Replacing a b s t
Replace \a -> b
ab -> (a ~> b) -> x' a ~> x' b
forall a b. (a ~> b) -> x' a ~> x' b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map ((a -> b) -> a -> b
f a -> b
ab) (x' a -> x' b) -> (x a -> x' a) -> x a -> x' b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x a ~> x' a
x a -> x' a
x .~> x'
w

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


newtype Classifying m a b s t = Classifying
  { forall {k} (m :: Type -> Type) (a :: k) b s t.
Classifying m a b s t -> Monad m => m s -> b -> t
getClassify :: (Monad m) => m s -> b -> t }
instance Monad m => Profunctor (Classifying m a b) where
  dimap :: forall c a b d.
(c ~> a)
-> (b ~> d) -> Classifying m a b a b -> Classifying m a b c d
dimap c ~> a
l b ~> d
r (Classifying Monad m => m a -> b -> b
f) = (Monad m => m c -> b -> d) -> Classifying m a b c d
forall {k} (m :: Type -> Type) (a :: k) b s t.
(Monad m => m s -> b -> t) -> Classifying m a b s t
Classifying (\m c
u -> b ~> d
b -> d
r (b -> d) -> (b -> b) -> b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. m a -> b -> b
Monad m => m a -> b -> b
f ((c -> a) -> m c -> m a
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap c ~> a
c -> a
l m c
u))
instance Monad m => Tambara (Sub :: CAT (SUBCAT (Algebra m))) (Classifying m a b) where
  tambara :: forall (x :: SUBCAT (Algebra m)) (x' :: SUBCAT (Algebra m)) a b.
Sub x x'
-> Classifying m a b a b -> Classifying m a b (Act x a) (Act x' b)
tambara (Sub a1 ~> b1
w) (Classifying Monad m => m a -> b -> b
f) = (Monad m => m (a1, a) -> b -> (b1, b))
-> Classifying m a b (a1, a) (b1, b)
forall {k} (m :: Type -> Type) (a :: k) b s t.
(Monad m => m s -> b -> t) -> Classifying m a b s t
Classifying (\m (a1, a)
m b
b -> (m b1 -> b1
forall (m :: Type -> Type) a. Algebra m a => m a -> a
algebra (((a1, a) -> b1) -> m (a1, a) -> m b1
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a1 ~> b1
a1 -> b1
w (a1 -> b1) -> ((a1, a) -> a1) -> (a1, a) -> b1
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a1, a) -> a1
forall a b. (a, b) -> a
fst) m (a1, a)
m), m a -> b -> b
Monad m => m a -> b -> b
f (((a1, a) -> a) -> m (a1, a) -> m a
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a1, a) -> a
forall a b. (a, b) -> b
snd m (a1, a)
m) b
b))

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