{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Enriched where

import Data.Kind (Constraint, Type)

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Instance.Constraint (CONSTRAINT (..), (:-) (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..))
import Proarrow.Core (Any, CAT, CategoryOf (..), Kind, Profunctor (..), type (+->))
import Proarrow.Monoid (MONOIDK (..), Mon (..), Monoid (..))
import Proarrow.Object.Exponential (uncurry)
import Proarrow.Object.Exponential qualified as E
import Proarrow.Category.Enriched.ThinCategory (CodiscreteProfunctor (..), ThinProfunctor (..))
import Proarrow.Profunctor qualified as P
import Proarrow.Category.Opposite (Op(..), OPPOSITE (..))

-- | Working with enriched categories and profunctors in Haskell is hard.
-- Instead we encode them using the underlying regular category/profunctor,
-- and show that the enriched structure can be recovered.
type EnrichedProfunctor :: forall {j} {k}. Kind -> j +-> k -> Constraint
class (Monoidal v, Profunctor p, Enriched v j, Enriched v k) => EnrichedProfunctor v (p :: j +-> k) where
  type ProObj v (p :: j +-> k) (a :: k) (b :: j) :: v
  withProObj :: (Ob (a :: k), Ob b) => ((Ob (ProObj v p a b)) => r) -> r
  underlying :: p a b -> Unit ~> ProObj v p a b
  enriched :: (Ob a, Ob b) => Unit ~> ProObj v p a b -> p a b
  rmap :: (Ob a, Ob b, Ob c) => HomObj v b c ** ProObj v p a b ~> ProObj v p a c
  lmap :: (Ob a, Ob b, Ob c) => HomObj v c a ** ProObj v p a b ~> ProObj v p c b

class (EnrichedProfunctor v ((~>) :: CAT k)) => Enriched v k
instance (EnrichedProfunctor v ((~>) :: CAT k)) => Enriched v k

type HomObj v (a :: k) (b :: k) = ProObj v ((~>) :: CAT k) a b

comp :: forall {k} v (a :: k) b c. (Enriched v k, Ob a, Ob b, Ob c) => HomObj v b c ** HomObj v a b ~> HomObj v a c
comp :: forall {k} v (a :: k) (b :: k) (c :: k).
(Enriched v k, Ob a, Ob b, Ob c) =>
(HomObj v b c ** HomObj v a b) ~> HomObj v a c
comp = forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) (c :: j).
(EnrichedProfunctor v p, Ob a, Ob b, Ob c) =>
(HomObj v b c ** ProObj v p a b) ~> ProObj v p a c
forall v (p :: k +-> k) (a :: k) (b :: k) (c :: k).
(EnrichedProfunctor v p, Ob a, Ob b, Ob c) =>
(HomObj v b c ** ProObj v p a b) ~> ProObj v p a c
rmap @v @((~>) :: CAT k) @a @b @c

-- | Closed monoidal categories are enriched in themselves.
type HomSelf a b = a E.~~> b

underlyingSelf :: (E.Closed k) => (a :: k) ~> b -> Unit ~> HomSelf a b
underlyingSelf :: forall k (a :: k) (b :: k).
Closed k =>
(a ~> b) -> Unit ~> HomSelf a b
underlyingSelf = (a ~> b) -> Unit ~> (a ~~> b)
forall k (a :: k) (b :: k).
Closed k =>
(a ~> b) -> Unit ~> HomSelf a b
E.mkExponential

enrichedSelf :: (E.Closed k, Ob (a :: k), Ob b) => Unit ~> HomSelf a b -> a ~> b
enrichedSelf :: forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
(Unit ~> HomSelf a b) -> a ~> b
enrichedSelf = (Unit ~> (a ~~> b)) -> a ~> b
forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
(Unit ~> HomSelf a b) -> a ~> b
E.lower

compSelf :: forall {k} (a :: k) b c. (E.Closed k, Ob a, Ob b, Ob c) => HomSelf b c ** HomSelf a b ~> HomSelf a c
compSelf :: forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b, Ob c) =>
(HomSelf b c ** HomSelf a b) ~> HomSelf a c
compSelf = forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b, Ob c) =>
((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b, Ob c) =>
(HomSelf b c ** HomSelf a b) ~> HomSelf a c
E.comp @a @b @c

-- abusing SUBCAT Any as a cheap wrapper to prevent overlapping instances
type Clone k = SUBCAT (Any :: k -> Constraint)

-- | A monoid is a one object enriched category.
instance (Monoid (m :: k)) => EnrichedProfunctor (Clone k) (Mon :: CAT (MONOIDK (m :: k))) where
  type ProObj (Clone k) (Mon :: CAT (MONOIDK m)) M M = SUB m
  withProObj :: forall (a :: MONOIDK m) (b :: MONOIDK m) r.
(Ob a, Ob b) =>
(Ob (ProObj (Clone k) Mon a b) => r) -> r
withProObj Ob (ProObj (Clone k) Mon a b) => r
r = r
Ob (ProObj (Clone k) Mon a b) => r
r
  underlying :: forall (a :: MONOIDK m) (b :: MONOIDK m).
Mon a b -> Unit ~> ProObj (Clone k) Mon a b
underlying (Mon Unit ~> m
f) = (Unit ~> m) -> Sub (~>) (SUB Unit) (SUB m)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub Unit ~> m
f
  enriched :: forall (a :: MONOIDK m) (b :: MONOIDK m).
(Ob a, Ob b) =>
(Unit ~> ProObj (Clone k) Mon a b) -> Mon a b
enriched (Sub a1 ~> b1
f) = (Unit ~> m) -> Mon M M
forall {k} {k1} {m1 :: k1} (m :: k). (Unit ~> m) -> Mon M M
Mon a1 ~> b1
Unit ~> m
f
  rmap :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b, Ob c) =>
(HomObj (Clone k) b c ** ProObj (Clone k) Mon a b)
~> ProObj (Clone k) Mon a c
rmap = ((m ** m) ~> m) -> Sub (~>) (SUB (m ** m)) (SUB m)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend
  lmap :: forall (a :: MONOIDK m) (b :: MONOIDK m) (c :: MONOIDK m).
(Ob a, Ob b, Ob c) =>
(HomObj (Clone k) c a ** ProObj (Clone k) Mon a b)
~> ProObj (Clone k) Mon c b
lmap = ((m ** m) ~> m) -> Sub (~>) (SUB (m ** m)) (SUB m)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend

instance (Profunctor p) => EnrichedProfunctor Type p where
  type ProObj Type p a b = p a b
  withProObj :: forall (a :: k) (b :: j) r.
(Ob a, Ob b) =>
(Ob (ProObj Type p a b) => r) -> r
withProObj Ob (ProObj Type p a b) => r
r = r
Ob (ProObj Type p a b) => r
r
  underlying :: forall (a :: k) (b :: j). p a b -> Unit ~> ProObj Type p a b
underlying p a b
p () = p a b
p
  enriched :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
(Unit ~> ProObj Type p a b) -> p a b
enriched Unit ~> ProObj Type p a b
f = Unit ~> ProObj Type p a b
() -> p a b
f ()
  rmap :: forall (a :: k) (b :: j) (c :: j).
(Ob a, Ob b, Ob c) =>
(HomObj Type b c ** ProObj Type p a b) ~> ProObj Type p a c
rmap = ((b ~> c) ~> (p a b ~~> p a c)) -> ((b ~> c) ** p a b) ~> p a c
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry (b ~> c) ~> (p a b ~~> p a c)
(b ~> c) -> p a b -> p a c
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
P.rmap
  lmap :: forall (a :: k) (b :: j) (c :: k).
(Ob a, Ob b, Ob c) =>
(HomObj Type c a ** ProObj Type p a b) ~> ProObj Type p c b
lmap = ((c ~> a) ~> (p a b ~~> p c b)) -> ((c ~> a) ** p a b) ~> p c b
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry (c ~> a) ~> (p a b ~~> p c b)
(c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
P.lmap

instance (DaggerProfunctor p) => EnrichedProfunctor (Type, Type) p where
  type ProObj (Type, Type) p a b = '(p a b, p b a)
  withProObj :: forall (a :: j) (b :: j) r.
(Ob a, Ob b) =>
(Ob (ProObj (Type, Type) p a b) => r) -> r
withProObj Ob (ProObj (Type, Type) p a b) => r
r = r
Ob (ProObj (Type, Type) p a b) => r
r
  underlying :: forall (a :: j) (b :: j).
p a b -> Unit ~> ProObj (Type, Type) p a b
underlying p a b
p = (\() -> p a b
p) (() -> p a b)
-> (() -> p b a) -> (:**:) (->) (->) '((), ()) '(p a b, p b a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (\() -> p a b -> p b a
forall (a :: j) (b :: j). p a b -> p b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger p a b
p)
  enriched :: forall (a :: j) (b :: j).
(Ob a, Ob b) =>
(Unit ~> ProObj (Type, Type) p a b) -> p a b
enriched (a1 -> b1
f :**: a2 -> b2
_) = a1 -> b1
() -> p a b
f ()
  rmap :: forall (a :: j) (b :: j) (c :: j).
(Ob a, Ob b, Ob c) =>
(HomObj (Type, Type) b c ** ProObj (Type, Type) p a b)
~> ProObj (Type, Type) p a c
rmap = ((b ~> c) ~> (p a b ~~> p a c)) -> ((b ~> c) ** p a b) ~> p a c
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry (b ~> c) ~> (p a b ~~> p a c)
(b ~> c) -> p a b -> p a c
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
P.rmap ((b ~> c, p a b) -> p a c)
-> ((c ~> b, p b a) -> p c a)
-> (:**:)
     (->) (->) '((b ~> c, p a b), (c ~> b, p b a)) '(p a c, p c a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: ((c ~> b) ~> (p b a ~~> p c a)) -> ((c ~> b) ** p b a) ~> p c a
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry (c ~> b) ~> (p b a ~~> p c a)
(c ~> b) -> p b a -> p c a
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
P.lmap
  lmap :: forall (a :: j) (b :: j) (c :: j).
(Ob a, Ob b, Ob c) =>
(HomObj (Type, Type) c a ** ProObj (Type, Type) p a b)
~> ProObj (Type, Type) p c b
lmap = ((c ~> a) ~> (p a b ~~> p c b)) -> ((c ~> a) ** p a b) ~> p c b
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry (c ~> a) ~> (p a b ~~> p c b)
(c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
P.lmap ((c ~> a, p a b) -> p c b)
-> ((a ~> c, p b a) -> p b c)
-> (:**:)
     (->) (->) '((c ~> a, p a b), (a ~> c, p b a)) '(p c b, p b c)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: ((a ~> c) ~> (p b a ~~> p b c)) -> ((a ~> c) ** p b a) ~> p b c
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry (a ~> c) ~> (p b a ~~> p b c)
(a ~> c) -> p b a -> p b c
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
P.rmap

instance (ThinProfunctor p) => EnrichedProfunctor CONSTRAINT p where
  type ProObj CONSTRAINT p a b = CNSTRNT (HasArrow p a b)
  withProObj :: forall (a :: k) (b :: j) r.
(Ob a, Ob b) =>
(Ob (ProObj CONSTRAINT p a b) => r) -> r
withProObj Ob (ProObj CONSTRAINT p a b) => r
r = r
Ob (ProObj CONSTRAINT p a b) => r
r
  underlying :: forall (a :: k) (b :: j). p a b -> Unit ~> ProObj CONSTRAINT p a b
underlying p a b
p = (forall r. (() :: Constraint) => (HasArrow p a b => r) -> r)
-> 'CNSTRNT (() :: Constraint) :- 'CNSTRNT (HasArrow p a b)
forall (a1 :: Constraint) (b1 :: Constraint).
(forall r. a1 => (b1 => r) -> r) -> 'CNSTRNT a1 :- 'CNSTRNT b1
Entails (\HasArrow p a b => r
r -> p a b -> (HasArrow p a b => r) -> r
forall (a :: k) (b :: j) r. p a b -> (HasArrow p a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr p a b
p r
HasArrow p a b => r
r)
  enriched :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
(Unit ~> ProObj CONSTRAINT p a b) -> p a b
enriched (Entails forall r. a1 => (b1 => r) -> r
f) = (b1 => p a b) -> p a b
forall r. a1 => (b1 => r) -> r
f p a b
b1 => p a b
forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow p a b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr
  rmap :: forall (a :: k) (b :: j) (c :: j).
(Ob a, Ob b, Ob c) =>
(HomObj CONSTRAINT b c ** ProObj CONSTRAINT p a b)
~> ProObj CONSTRAINT p a c
rmap @a @b @c = (forall r.
 (HasArrow (~>) b c, HasArrow p a b) =>
 (HasArrow p a c => r) -> r)
-> 'CNSTRNT (HasArrow (~>) b c, HasArrow p a b)
   :- 'CNSTRNT (HasArrow p a c)
forall (a1 :: Constraint) (b1 :: Constraint).
(forall r. a1 => (b1 => r) -> r) -> 'CNSTRNT a1 :- 'CNSTRNT b1
Entails (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
forall (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr @p ((b ~> c) -> p a b -> p a c
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
P.rmap (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: j +-> j) (a :: j) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @(~>) @b @c) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @p @a @b)))
  lmap :: forall (a :: k) (b :: j) (c :: k).
(Ob a, Ob b, Ob c) =>
(HomObj CONSTRAINT c a ** ProObj CONSTRAINT p a b)
~> ProObj CONSTRAINT p c b
lmap @a @b @c = (forall r.
 (HasArrow (~>) c a, HasArrow p a b) =>
 (HasArrow p c b => r) -> r)
-> 'CNSTRNT (HasArrow (~>) c a, HasArrow p a b)
   :- 'CNSTRNT (HasArrow p c b)
forall (a1 :: Constraint) (b1 :: Constraint).
(forall r. a1 => (b1 => r) -> r) -> 'CNSTRNT a1 :- 'CNSTRNT b1
Entails (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
forall (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr @p ((c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
P.lmap (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: k +-> k) (a :: k) (b :: k).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @(~>) @c @a) (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
forall (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @p @a @b)))

instance (CodiscreteProfunctor p) => EnrichedProfunctor () p where
  type ProObj () p a b = '()
  withProObj :: forall (a :: k) (b :: j) r.
(Ob a, Ob b) =>
(Ob (ProObj () p a b) => r) -> r
withProObj Ob (ProObj () p a b) => r
r = r
Ob (ProObj () p a b) => r
r
  underlying :: forall (a :: k) (b :: j). p a b -> Unit ~> ProObj () p a b
underlying p a b
_ = Unit ~> ProObj () p a b
Unit '() '()
U.Unit
  enriched :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
(Unit ~> ProObj () p a b) -> p a b
enriched Unit ~> ProObj () p a b
Unit '() '()
U.Unit = p a b
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(CodiscreteProfunctor p, Ob a, Ob b) =>
p a b
anyArr
  rmap :: forall (a :: k) (b :: j) (c :: j).
(Ob a, Ob b, Ob c) =>
(HomObj () b c ** ProObj () p a b) ~> ProObj () p a c
rmap = (ProObj () (~>) b c ** ProObj () p a b) ~> ProObj () p a c
Unit '() '()
U.Unit
  lmap :: forall (a :: k) (b :: j) (c :: k).
(Ob a, Ob b, Ob c) =>
(HomObj () c a ** ProObj () p a b) ~> ProObj () p c b
lmap = (ProObj () (~>) c a ** ProObj () p a b) ~> ProObj () p c b
Unit '() '()
U.Unit

instance (EnrichedProfunctor v p) => EnrichedProfunctor (Clone v) (Op p) where
  type ProObj (Clone v) (Op p) (OP a) (OP b) = SUB (ProObj v p b a)
  withProObj :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) r.
(Ob a, Ob b) =>
(Ob (ProObj (Clone v) (Op p) a b) => r) -> r
withProObj @(OP a) @(OP b) Ob (ProObj (Clone v) (Op p) a b) => r
r = forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @v @p @b @a r
Ob (ProObj v p (UN 'OP b) (UN 'OP a)) => r
Ob (ProObj (Clone v) (Op p) a b) => r
r
  underlying :: forall (a :: OPPOSITE j) (b :: OPPOSITE k).
Op p a b -> Unit ~> ProObj (Clone v) (Op p) a b
underlying (Op p b1 a1
f) = (Unit ~> ProObj v p b1 a1)
-> Sub (~>) (SUB Unit) (SUB (ProObj v p b1 a1))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j).
EnrichedProfunctor v p =>
p a b -> Unit ~> ProObj v p a b
forall v (p :: j +-> k) (a :: k) (b :: j).
EnrichedProfunctor v p =>
p a b -> Unit ~> ProObj v p a b
underlying @v @p p b1 a1
f)
  enriched :: forall (a :: OPPOSITE j) (b :: OPPOSITE k).
(Ob a, Ob b) =>
(Unit ~> ProObj (Clone v) (Op p) a b) -> Op p a b
enriched (Sub a1 ~> b1
f) = p (UN 'OP b) (UN 'OP a) -> Op p ('OP (UN 'OP a)) ('OP (UN 'OP b))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op ((Unit ~> ProObj v p (UN 'OP b) (UN 'OP a))
-> p (UN 'OP b) (UN 'OP a)
forall (a :: k) (b :: j).
(Ob a, Ob b) =>
(Unit ~> ProObj v p a b) -> p a b
forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j).
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Unit ~> ProObj v p a b) -> p a b
enriched a1 ~> b1
Unit ~> ProObj v p (UN 'OP b) (UN 'OP a)
f)
  rmap :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) (c :: OPPOSITE k).
(Ob a, Ob b, Ob c) =>
(HomObj (Clone v) b c ** ProObj (Clone v) (Op p) a b)
~> ProObj (Clone v) (Op p) a c
rmap @(OP a) @(OP b) @(OP c) = ((ProObj v (~>) (UN 'OP c) (UN 'OP b)
  ** ProObj v p (UN 'OP b) (UN 'OP a))
 ~> ProObj v p (UN 'OP c) (UN 'OP a))
-> Sub
     (~>)
     (SUB
        (ProObj v (~>) (UN 'OP c) (UN 'OP b)
         ** ProObj v p (UN 'OP b) (UN 'OP a)))
     (SUB (ProObj v p (UN 'OP c) (UN 'OP a)))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) (c :: k).
(EnrichedProfunctor v p, Ob a, Ob b, Ob c) =>
(HomObj v c a ** ProObj v p a b) ~> ProObj v p c b
forall v (p :: j +-> k) (a :: k) (b :: j) (c :: k).
(EnrichedProfunctor v p, Ob a, Ob b, Ob c) =>
(HomObj v c a ** ProObj v p a b) ~> ProObj v p c b
lmap @v @p @b @a @c)
  lmap :: forall (a :: OPPOSITE j) (b :: OPPOSITE k) (c :: OPPOSITE j).
(Ob a, Ob b, Ob c) =>
(HomObj (Clone v) c a ** ProObj (Clone v) (Op p) a b)
~> ProObj (Clone v) (Op p) c b
lmap @(OP a) @(OP b) @(OP c) = ((ProObj v (~>) (UN 'OP a) (UN 'OP c)
  ** ProObj v p (UN 'OP b) (UN 'OP a))
 ~> ProObj v p (UN 'OP b) (UN 'OP c))
-> Sub
     (~>)
     (SUB
        (ProObj v (~>) (UN 'OP a) (UN 'OP c)
         ** ProObj v p (UN 'OP b) (UN 'OP a)))
     (SUB (ProObj v p (UN 'OP b) (UN 'OP c)))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) (c :: j).
(EnrichedProfunctor v p, Ob a, Ob b, Ob c) =>
(HomObj v b c ** ProObj v p a b) ~> ProObj v p a c
forall v (p :: j +-> k) (a :: k) (b :: j) (c :: j).
(EnrichedProfunctor v p, Ob a, Ob b, Ob c) =>
(HomObj v b c ** ProObj v p a b) ~> ProObj v p a c
rmap @v @p @b @a @c)