{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The monoidal category of endo-profunctors on @k@ under composition ('(:.:)'\/'Id'),
-- with functor composition as the tensor. This is the profunctor-specific counterpart of
-- "Proarrow.Category.Monoidal.Endo" (in @proarrow-equipment@, which builds the analogous
-- structure for an arbitrary 'Proarrow.Bicategory.Bicategory'), hardcoded here to
-- @Prof@\/@:.:@\/'Id' instead, and reusing "Proarrow.Path"\'s associators\/unitors so they
-- aren't proved twice.
--
-- Note this is a genuinely different monoidal structure on @k +-> k@ than
-- "Proarrow.Profunctor.Instance.Day"\'s @Monoidal (j +-> k)@ instance (Day convolution) --
-- hence the need for a fresh wrapper type rather than another instance for the same kind.
module Proarrow.Category.Monoidal.EndoProf where

import Data.Kind (Constraint, Type)

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..))
import Proarrow.Category.Monoidal.Distributive (Traversable)
import Proarrow.Category.Monoidal.Rev (REV (..), Rev (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, OB, Profunctor (..), Promonad (..), UN, type (+->), type (:~>))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Optic (type (:&&:))
import Proarrow.Path qualified as Path
import Proarrow.Profunctor.Instance.Composition (o, (:.:))
import Proarrow.Profunctor.Instance.Identity (Id)
import Proarrow.Profunctor.Representable (Rep (..), Representable (..), index, repMap, repUniv, withObRep)

-- | An object of @'ENDO' k@ is an endo-profunctor @k +-> k@, i.e. (not necessarily
-- representable) a functor @k -> k@ under the profunctor encoding.
type ENDO :: Type -> Type
type data ENDO k = E (k +-> k)

-- | Morphisms of @'ENDO' k@ are natural transformations between the underlying profunctors.
type Endo :: CAT (ENDO k)
data Endo p q where
  Endo :: (Profunctor p, Profunctor q) => (p :~> q) -> Endo (E p) (E q)

instance (CategoryOf k) => Profunctor (Endo :: CAT (ENDO k)) where
  dimap :: forall (c :: ENDO k) (a :: ENDO k) (b :: ENDO k) (d :: ENDO k).
(c ~> a) -> (b ~> d) -> Endo a b -> Endo c d
dimap (Endo p :~> q
l) (Endo p :~> q
r) (Endo p :~> q
f) = (p :~> q) -> Endo (E p) (E q)
forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Endo (E p) (E q)
Endo (p a b -> q a b
p :~> q
r (p a b -> q a b) -> (p a b -> p a b) -> p a b -> q a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. q a b -> p a b
p a b -> q a b
p :~> q
f (q a b -> p a b) -> (p a b -> q a b) -> p a b -> p a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b -> q a b
p :~> q
l)
  (Ob a, Ob b) => r
r \\ :: forall (a :: ENDO k) (b :: ENDO k) r.
((Ob a, Ob b) => r) -> Endo a b -> r
\\ Endo p :~> q
_ = r
(Ob a, Ob b) => r
r

instance (CategoryOf k) => Promonad (Endo :: CAT (ENDO k)) where
  id :: forall (a :: ENDO k). Ob a => Endo a a
id = (UN E a :~> UN E a) -> Endo (E (UN E a)) (E (UN E a))
forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Endo (E p) (E q)
Endo UN E a a b -> UN E a a b
UN E a :~> UN E a
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
Path.idN
  Endo p :~> q
f . :: forall (b :: ENDO k) (c :: ENDO k) (a :: ENDO k).
Endo b c -> Endo a b -> Endo a c
. Endo p :~> q
g = (p :~> q) -> Endo (E p) (E q)
forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Endo (E p) (E q)
Endo (p a b -> q a b
p :~> q
f (p a b -> q a b) -> (p a b -> p a b) -> p a b -> q a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b -> p a b
p a b -> q a b
p :~> q
g)

-- | The category of endoprofunctors on @k@ and natural transformations between them.
instance (CategoryOf k) => CategoryOf (ENDO k) where
  type (~>) = Endo
  type Ob (a :: ENDO k) = (Is E a, Profunctor (UN E a))

instance (CategoryOf k) => MonoidalProfunctor (Endo :: CAT (ENDO k)) where
  one :: Endo Unit Unit
one = (Id :~> Id) -> Endo (E Id) (E Id)
forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Endo (E p) (E q)
Endo Id a b -> Id a b
Id :~> Id
forall {k} {k1} (p :: k -> k1 -> Type) (a :: k) (b :: k1).
p a b -> p a b
Path.idN
  Endo p :~> q
f ** :: forall (x1 :: ENDO k) (x2 :: ENDO k) (y1 :: ENDO k) (y2 :: ENDO k).
Endo x1 x2 -> Endo y1 y2 -> Endo (x1 ** y1) (x2 ** y2)
** Endo p :~> q
g = ((p :.: p) :~> (q :.: q)) -> Endo (E (p :.: p)) (E (q :.: q))
forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Endo (E p) (E q)
Endo (p a b -> q a b
p :~> q
f (p :~> q) -> (p :~> q) -> (p :.: p) :~> (q :.: q)
forall {i} {j} {k} (p :: j +-> k) (q :: j +-> k) (r :: i +-> j)
       (s :: i +-> j).
(p :~> q) -> (r :~> s) -> (p :.: r) :~> (q :.: s)
`o` p a b -> q a b
p :~> q
g)

instance (CategoryOf k) => Monoidal (ENDO k) where
  type Unit = E Id
  type E p ** E q = E (p :.: q)
  withOb2 :: forall (a :: ENDO k) (b :: ENDO k) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(E _) @(E _) Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: ENDO k). Ob a => (Unit ** a) ~> a
leftUnitor @(E p) = ((Id :.: UN E a) :~> UN E a)
-> Endo (E (Id :.: UN E a)) (E (UN E a))
forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Endo (E p) (E q)
Endo (forall {k1} {k} (p :: k1 +-> k). Profunctor p => (Id :.: p) :~> p
forall (p :: k +-> k). Profunctor p => (Id :.: p) :~> p
Path.leftUnitor @p)
  leftUnitorInv :: forall (a :: ENDO k). Ob a => a ~> (Unit ** a)
leftUnitorInv @(E p) = (UN E a :~> (Id :.: UN E a))
-> Endo (E (UN E a)) (E (Id :.: UN E a))
forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Endo (E p) (E q)
Endo (forall {i} {j} (p :: i +-> j). Profunctor p => p :~> (Id :.: p)
forall (p :: k +-> k). Profunctor p => p :~> (Id :.: p)
Path.leftUnitorInv @p)
  rightUnitor :: forall (a :: ENDO k). Ob a => (a ** Unit) ~> a
rightUnitor @(E p) = ((UN E a :.: Id) :~> UN E a)
-> Endo (E (UN E a :.: Id)) (E (UN E a))
forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Endo (E p) (E q)
Endo (forall {k1} {k} (p :: k1 +-> k). Profunctor p => (p :.: Id) :~> p
forall (p :: k +-> k). Profunctor p => (p :.: Id) :~> p
Path.rightUnitor @p)
  rightUnitorInv :: forall (a :: ENDO k). Ob a => a ~> (a ** Unit)
rightUnitorInv @(E p) = (UN E a :~> (UN E a :.: Id))
-> Endo (E (UN E a)) (E (UN E a :.: Id))
forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Endo (E p) (E q)
Endo (forall {i} {k} (p :: i +-> k). Profunctor p => p :~> (p :.: Id)
forall (p :: k +-> k). Profunctor p => p :~> (p :.: Id)
Path.rightUnitorInv @p)
  associator :: forall (a :: ENDO k) (b :: ENDO k) (c :: ENDO k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(E p) @(E q) @(E r) = (((UN E a :.: UN E b) :.: UN E c)
 :~> (UN E a :.: (UN E b :.: UN E c)))
-> Endo
     (E ((UN E a :.: UN E b) :.: UN E c))
     (E (UN E a :.: (UN E b :.: UN E c)))
forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Endo (E p) (E q)
Endo (forall {k1} {k2} {j} {i} (p :: k1 +-> k2) (q :: j +-> k1)
       (r :: i +-> j) (a :: k2) (b :: i).
(:.:) (p :.: q) r a b -> (:.:) p (q :.: r) a b
forall (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (a :: k)
       (b :: k).
(:.:) (p :.: q) r a b -> (:.:) p (q :.: r) a b
Path.associator @p @q @r)
  associatorInv :: forall (a :: ENDO k) (b :: ENDO k) (c :: ENDO k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(E p) @(E q) @(E r) = ((UN E a :.: (UN E b :.: UN E c))
 :~> ((UN E a :.: UN E b) :.: UN E c))
-> Endo
     (E (UN E a :.: (UN E b :.: UN E c)))
     (E ((UN E a :.: UN E b) :.: UN E c))
forall {k1} (p :: k1 +-> k1) (q :: k1 +-> k1).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Endo (E p) (E q)
Endo (forall {j1} {k} {j2} {i} (p :: j1 +-> k) (q :: j2 +-> j1)
       (r :: i +-> j2) (a :: k) (b :: i).
(:.:) p (q :.: r) a b -> (:.:) (p :.: q) r a b
forall (p :: k +-> k) (q :: k +-> k) (r :: k +-> k) (a :: k)
       (b :: k).
(:.:) p (q :.: r) a b -> (:.:) (p :.: q) r a b
Path.associatorInv @p @q @r)

-- | Lift a constraint on profunctors @k +-> k@ to the corresponding 'ENDO' objects.
type OnE :: ((k +-> k) -> Constraint) -> ENDO k -> Constraint
class (Is E a, c (UN E a)) => OnE c a

instance (Is E a, c (UN E a)) => OnE c a

-- | The subcategory of representable endo-profunctors -- i.e. ordinary functors
-- @k -> k@ under the profunctor encoding. The most permissive restriction of 'ENDO' for
-- which an 'Proarrow.Category.Monoidal.Action.Act'ion even makes sense (@'%'@ needs
-- 'Representable'), so every other 'MonoidalAction' on @k@ embeds into this one -- see
-- 'TravSub' for a further restriction.
type RepSub k = SUBCAT (OnE Representable :: OB (ENDO k))

-- | The action of 'RepSub' on @k@ by application: @'Proarrow.Category.Monoidal.Action.Act' 'RepAction' ('SUB' ('E' f)) x = f '%' x@.
type RepAction = Rep RepAction'

data family RepAction' :: (RepSub k, k) +-> k
instance (CategoryOf k) => FunctorForRep (RepAction' :: (RepSub k, k) +-> k) where
  type RepAction' @ '(SUB (E p), x) = p % x
  fmap :: forall (a :: (RepSub k, k)) (b :: (RepSub k, k)).
(a ~> b) -> (RepAction' @ a) ~> (RepAction' @ b)
fmap (Sub (Endo @p @q p :~> q
n) :**: (a2 ~> b2
g :: x ~> y)) = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index @q (p (UN E a1 % b2) b2 -> q (UN E a1 % b2) b2
p :~> q
n (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k +-> k) (a :: k).
(Representable p, Ob a) =>
p (p % a) a
repUniv @p @y)) ((UN E a1 % b2) ~> (UN E b1 % b2))
-> ((UN E a1 % a2) ~> (UN E a1 % b2))
-> (UN E a1 % a2) ~> (UN E b1 % b2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a2 ~> b2
g ((Ob a2, Ob b2) => (UN E a1 % a2) ~> (UN E b1 % b2))
-> (a2 ~> b2) -> (UN E a1 % a2) ~> (UN E b1 % b2)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a2 ~> b2
g

instance (CategoryOf k) => MonoidalAction (RepAction :: (RepSub k, k) +-> k) where
  unitor :: forall (x :: k). Ob x => Act RepAction Unit x ~> x
unitor = x ~> x
(RepAction % '(Unit, x)) ~> x
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  unitorInv :: forall (x :: k). Ob x => x ~> Act RepAction Unit x
unitorInv = x ~> x
x ~> (RepAction % '(Unit, x))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  multiplicator :: forall (a :: RepSub k) (b :: RepSub k) (x :: k).
(Ob a, Ob b, Ob x) =>
Act RepAction (a ** b) x ~> Act RepAction a (Act RepAction b x)
multiplicator @(SUB (E p)) @(SUB (E q)) @x = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> k) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @q @x (forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> k) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @(q % x) (UN E (UN SUB a) % (UN E (UN SUB b) % x))
~> (UN E (UN SUB a) % (UN E (UN SUB b) % x))
Ob (UN E (UN SUB a) % (UN E (UN SUB b) % x)) =>
(UN E (UN SUB a) % (UN E (UN SUB b) % x))
~> (UN E (UN SUB a) % (UN E (UN SUB b) % x))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
  multiplicatorInv :: forall (a :: RepSub k) (b :: RepSub k) (x :: k).
(Ob a, Ob b, Ob x) =>
Act RepAction a (Act RepAction b x) ~> Act RepAction (a ** b) x
multiplicatorInv @(SUB (E p)) @(SUB (E q)) @x = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> k) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @q @x (forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> k) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @(q % x) (UN E (UN SUB a) % (UN E (UN SUB b) % x))
~> (UN E (UN SUB a) % (UN E (UN SUB b) % x))
Ob (UN E (UN SUB a) % (UN E (UN SUB b) % x)) =>
(UN E (UN SUB a) % (UN E (UN SUB b) % x))
~> (UN E (UN SUB a) % (UN E (UN SUB b) % x))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)

-- | The subcategory of representable, traversable endo-profunctors -- exactly the
-- functors 'Proarrow.Category.Monoidal.Distributive.repTraverse' can traverse with.
-- 'Monoidal' for free via "Proarrow.Category.Instance.Sub"\'s generic
-- @Monoidal (SUBCAT ob)@, since both 'Representable' and 'Traversable' already have
-- instances closing them under @:.:@\/'Id'.
type TravSub k = SUBCAT (OnE (Representable :&&: Traversable) :: OB (ENDO k))

-- | The action of 'TravSub' on @k@ by application: @'Proarrow.Category.Monoidal.Action.Act' 'TravAction' ('SUB' ('E' f)) x = f '%' x@.
type TravAction = Rep TravAction'

data family TravAction' :: (TravSub k, k) +-> k
instance (CategoryOf k) => FunctorForRep (TravAction' :: (TravSub k, k) +-> k) where
  type TravAction' @ '(SUB (E p), x) = p % x
  fmap :: forall (a :: (TravSub k, k)) (b :: (TravSub k, k)).
(a ~> b) -> (TravAction' @ a) ~> (TravAction' @ b)
fmap (Sub (Endo @p @q p :~> q
n) :**: (a2 ~> b2
g :: x ~> y)) = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index @q (p (UN E a1 % b2) b2 -> q (UN E a1 % b2) b2
p :~> q
n (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k +-> k) (a :: k).
(Representable p, Ob a) =>
p (p % a) a
repUniv @p @y)) ((UN E a1 % b2) ~> (UN E b1 % b2))
-> ((UN E a1 % a2) ~> (UN E a1 % b2))
-> (UN E a1 % a2) ~> (UN E b1 % b2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a2 ~> b2
g ((Ob a2, Ob b2) => (UN E a1 % a2) ~> (UN E b1 % b2))
-> (a2 ~> b2) -> (UN E a1 % a2) ~> (UN E b1 % b2)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a2 ~> b2
g

instance (CategoryOf k) => MonoidalAction (TravAction :: (TravSub k, k) +-> k) where
  unitor :: forall (x :: k). Ob x => Act TravAction Unit x ~> x
unitor = x ~> x
(TravAction % '(Unit, x)) ~> x
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  unitorInv :: forall (x :: k). Ob x => x ~> Act TravAction Unit x
unitorInv = x ~> x
x ~> (TravAction % '(Unit, x))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  multiplicator :: forall (a :: TravSub k) (b :: TravSub k) (x :: k).
(Ob a, Ob b, Ob x) =>
Act TravAction (a ** b) x ~> Act TravAction a (Act TravAction b x)
multiplicator @(SUB (E p)) @(SUB (E q)) @x = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> k) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @q @x (forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> k) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @(q % x) (UN E (UN SUB a) % (UN E (UN SUB b) % x))
~> (UN E (UN SUB a) % (UN E (UN SUB b) % x))
Ob (UN E (UN SUB a) % (UN E (UN SUB b) % x)) =>
(UN E (UN SUB a) % (UN E (UN SUB b) % x))
~> (UN E (UN SUB a) % (UN E (UN SUB b) % x))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
  multiplicatorInv :: forall (a :: TravSub k) (b :: TravSub k) (x :: k).
(Ob a, Ob b, Ob x) =>
Act TravAction a (Act TravAction b x) ~> Act TravAction (a ** b) x
multiplicatorInv @(SUB (E p)) @(SUB (E q)) @x = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> k) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @q @x (forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: k +-> k) (a :: k) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withObRep @p @(q % x) (UN E (UN SUB a) % (UN E (UN SUB b) % x))
~> (UN E (UN SUB a) % (UN E (UN SUB b) % x))
Ob (UN E (UN SUB a) % (UN E (UN SUB b) % x)) =>
(UN E (UN SUB a) % (UN E (UN SUB b) % x))
~> (UN E (UN SUB a) % (UN E (UN SUB b) % x))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)

-- | Endo-profunctors on @x@ (any, not just representable ones) act on profunctors
-- @x +-> h@ by precomposition: @'Proarrow.Category.Monoidal.Action.Act' 'Precomp' ('E' g) q = q ':.:' g@. Unlike 'RepAction'\/
-- 'TravAction', the acted-upon kind here isn't @x@ or @h@ itself but the whole profunctor
-- kind @x +-> h@, so the witness @g@ never has to be 'Representable' -- only the assembled
-- action (@'Rep' 'Precomp'@) does, which is automatic. This is what lets
-- 'Proarrow.Squares.toPrecompOptic' turn /any/ 'Proarrow.Squares.OpticSq' (not just ones
-- already shaped like an 'Proarrow.Category.Monoidal.Action.Act'ion) into a genuine
-- 'Proarrow.Optic.Optic'.
--
-- The index category is @'REV' ('ENDO' x)@, not @'ENDO' x@, because precomposition
-- reverses the order composition happens in: @'Proarrow.Category.Monoidal.**'@ on
-- @'ENDO' x@ composes its two arguments left-to-right, but composing two precomposition
-- actions in sequence applies them right-to-left.
data family Precomp :: forall x h. (REV (ENDO x), x +-> h) +-> (x +-> h)

instance (CategoryOf h, CategoryOf x) => FunctorForRep (Precomp :: (REV (ENDO x), x +-> h) +-> (x +-> h)) where
  type Precomp @ '(R (E g), q) = q :.: g
  fmap :: forall (a :: (REV (ENDO x), x +-> h))
       (b :: (REV (ENDO x), x +-> h)).
(a ~> b) -> (Precomp @ a) ~> (Precomp @ b)
fmap (Rev (Endo p :~> q
n) :**: Prof a2 :~> b2
h') = ((a2 :.: p) :~> (b2 :.: q)) -> Prof (a2 :.: p) (b2 :.: q)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (a2 a b -> b2 a b
a2 :~> b2
h' (a2 :~> b2) -> (p :~> q) -> (a2 :.: p) :~> (b2 :.: q)
forall {i} {j} {k} (p :: j +-> k) (q :: j +-> k) (r :: i +-> j)
       (s :: i +-> j).
(p :~> q) -> (r :~> s) -> (p :.: r) :~> (q :.: s)
`o` p a b -> q a b
p :~> q
n)

instance (CategoryOf h, CategoryOf x) => MonoidalAction (Rep Precomp :: (REV (ENDO x), x +-> h) +-> (x +-> h)) where
  unitor :: forall (x :: x +-> h). Ob x => Act (Rep Precomp) Unit x ~> x
unitor = ((x :.: Id) :~> x) -> Prof (x :.: Id) x
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (:.:) x Id a b -> x a b
(x :.: Id) :~> x
forall {k1} {k} (p :: k1 +-> k). Profunctor p => (p :.: Id) :~> p
Path.rightUnitor
  unitorInv :: forall (x :: x +-> h). Ob x => x ~> Act (Rep Precomp) Unit x
unitorInv = (x :~> (x :.: Id)) -> Prof x (x :.: Id)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof x a b -> (:.:) x Id a b
x :~> (x :.: Id)
forall {i} {k} (p :: i +-> k). Profunctor p => p :~> (p :.: Id)
Path.rightUnitorInv
  multiplicator :: forall (a :: REV (ENDO x)) (b :: REV (ENDO x)) (x :: x +-> h).
(Ob a, Ob b, Ob x) =>
Act (Rep Precomp) (a ** b) x
~> Act (Rep Precomp) a (Act (Rep Precomp) b x)
multiplicator @(R (E g)) @(R (E g')) @q = ((x :.: (UN E (UN R b) :.: UN E (UN R a)))
 :~> ((x :.: UN E (UN R b)) :.: UN E (UN R a)))
-> Prof
     (x :.: (UN E (UN R b) :.: UN E (UN R a)))
     ((x :.: UN E (UN R b)) :.: UN E (UN R a))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (forall {j1} {k} {j2} {i} (p :: j1 +-> k) (q :: j2 +-> j1)
       (r :: i +-> j2) (a :: k) (b :: i).
(:.:) p (q :.: r) a b -> (:.:) (p :.: q) r a b
forall (p :: x +-> h) (q :: x +-> x) (r :: x +-> x) (a :: h)
       (b :: x).
(:.:) p (q :.: r) a b -> (:.:) (p :.: q) r a b
Path.associatorInv @q @g' @g)
  multiplicatorInv :: forall (a :: REV (ENDO x)) (b :: REV (ENDO x)) (x :: x +-> h).
(Ob a, Ob b, Ob x) =>
Act (Rep Precomp) a (Act (Rep Precomp) b x)
~> Act (Rep Precomp) (a ** b) x
multiplicatorInv @(R (E g)) @(R (E g')) @q = (((x :.: UN E (UN R b)) :.: UN E (UN R a))
 :~> (x :.: (UN E (UN R b) :.: UN E (UN R a))))
-> Prof
     ((x :.: UN E (UN R b)) :.: UN E (UN R a))
     (x :.: (UN E (UN R b) :.: UN E (UN R a)))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof (forall {k1} {k2} {j} {i} (p :: k1 +-> k2) (q :: j +-> k1)
       (r :: i +-> j) (a :: k2) (b :: i).
(:.:) (p :.: q) r a b -> (:.:) p (q :.: r) a b
forall (p :: x +-> h) (q :: x +-> x) (r :: x +-> x) (a :: h)
       (b :: x).
(:.:) (p :.: q) r a b -> (:.:) p (q :.: r) a b
Path.associator @q @g' @g)