{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Categories and profunctors enriched in a monoidal category @v@, encoded via their underlying
-- ordinary category\/profunctor: 'EnrichedProfunctor' equips a regular profunctor with hom-objects
-- @'ProObj' v p a b@ in @v@ from which the enriched structure is recovered, and a category is
-- 'Enriched' when its hom-profunctor is. Instances include the self-enrichment of a
-- 'Proarrow.Category.Monoidal.Closed.Closed' category.
module Proarrow.Category.Enriched where

import Data.Kind (Constraint, Type)

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Enriched.Finitary (Elt (..), Finitary, LocallyFinite)
import Proarrow.Category.Enriched.Thin
  ( CodiscreteProfunctor (..)
  , Decidable
  , DecidableProfunctor (..)
  , Decision (..)
  , Thin
  , ThinProfunctor (..)
  )
import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
import Proarrow.Category.Instance.Constraint (CONSTRAINT (..), (:-) (..))
import Proarrow.Category.Instance.FinHask (FINHASK (..))
import Proarrow.Category.Instance.FinHask qualified as F
import Proarrow.Category.Instance.Monoid (MONOID (..), Mon (..))
import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof)
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), SymMonoidal (..), leftUnitorInvWith, rightUnitorInvWith)
import Proarrow.Category.Monoidal.Closed qualified as E
import Proarrow.Core (Any, CAT, CategoryOf (..), Hom, Kind, Profunctor ((\\)), Promonad (..), type (+->))
import Proarrow.Core qualified as P
import Proarrow.Limit.BinaryProduct (PROD, Prod)
import Proarrow.Monoid (Monoid (..))
import Proarrow.Profunctor.Instance.Exponential ()

-- | 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.
--
-- Call an arrow @'Unit' '~>' x@ an /element/ of @x@. The laws say that the elements of
-- @'ProObj' v p a b@ are those of the hom-set @p a b@, and that its two actions are the
-- profunctor's:
--
-- [Elements] 'underlying' and 'enriched' are mutually inverse, so 'underlying' is a bijection from
-- @p a b@ onto the elements of @'ProObj' v p a b@.
--
-- [Right action] for @f :: b '~>' c@ in @j@ and @x :: p a b@, where @'underlying' f@ names @f@ as
-- an element of @'HomObj' v b c@:
--
-- > rmap . (underlying f ** underlying x) . leftUnitorInv == underlying (P.rmap f x)
--
-- [Left action] dually, for @g :: c '~>' a@ in @k@:
--
-- > lmap . (underlying g ** underlying x) . leftUnitorInv == underlying (P.lmap g x)
--
-- These fix 'rmap' and 'lmap' completely iff @v@ is well-pointed, as 'Type' and the thin @v@s are.
-- Functoriality follows from the 'Profunctor' instance. At @p ~ 'Hom' k@ the right-action law says
-- that the enriched composition 'comp' is @('.')@.
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 (Hom k)) => Enriched v k
instance (EnrichedProfunctor v (Hom k)) => Enriched v k

type HomObj v (a :: k) (b :: k) = ProObj v (Hom 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 @(Hom 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 (MONOID (m :: k))) where
  type ProObj (Clone k) (Mon :: CAT (MONOID m)) M M = SUB m
  withProObj :: forall (a :: MONOID m) (b :: MONOID 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 :: MONOID m) (b :: MONOID 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 :: MONOID m) (b :: MONOID 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 :: MONOID m) (b :: MONOID m) (c :: MONOID 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 :: MONOID m) (b :: MONOID m) (c :: MONOID 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
E.uncurry (b ~> c) ~> (p a b ~~> p a c)
(b ~> c) -> p a b -> p a c
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
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
E.uncurry (c ~> a) ~> (p a b ~~> p c b)
(c ~> a) -> p a b -> p c b
forall (c :: k) (a :: k) (b :: j). (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
E.uncurry (b ~> c) ~> (p a b ~~> p a c)
(b ~> c) -> p a b -> p a c
forall (b :: j) (d :: j) (a :: j). (b ~> d) -> p a b -> p a d
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
E.uncurry (c ~> b) ~> (p b a ~~> p c a)
(c ~> b) -> p b a -> p c a
forall (c :: j) (a :: j) (b :: j). (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
  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
E.uncurry (c ~> a) ~> (p a b ~~> p c b)
(c ~> a) -> p a b -> p c b
forall (c :: j) (a :: j) (b :: j). (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
E.uncurry (a ~> c) ~> (p b a ~~> p b c)
(a ~> c) -> p b a -> p b c
forall (b :: j) (d :: j) (a :: j). (b ~> d) -> p a b -> p a d
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, Thin j, Thin k) => EnrichedProfunctor CONSTRAINT (p :: j +-> k) 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, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: j) r.
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr p a b
p r
HasArrow p a b => r
(HasArrow p a b, Ob a, Ob 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 (Hom j) b c, HasArrow p a b) =>
 (HasArrow p a c => r) -> r)
-> CNSTRNT (HasArrow (Hom j) 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 \HasArrow p a c => r
r -> forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr @p ((b ~> c) -> p a b -> p a c
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
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)) r
HasArrow p a c => r
(HasArrow p a c, Ob a, Ob c) => r
r
  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 (Hom k) c a, HasArrow p a b) =>
 (HasArrow p c b => r) -> r)
-> CNSTRNT (HasArrow (Hom k) 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 \HasArrow p c b => r
r -> forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr @p ((c ~> a) -> p a b -> p c b
forall (c :: k) (a :: k) (b :: j). (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)) r
HasArrow p c b => r
(HasArrow p c b, Ob c, Ob b) => r
r

-- | A decidable thin profunctor is a profunctor enriched in the walking arrow: its hom-object is the
-- type-level 'Holds', an element of it is an arrow, and composition is conjunction.
instance (DecidableProfunctor p, Decidable j, Decidable k) => EnrichedProfunctor BOOL (p :: j +-> k) where
  type ProObj BOOL p a b = Holds p a b
  withProObj :: forall (a :: k) (b :: j) r.
(Ob a, Ob b) =>
(Ob (ProObj BOOL p a b) => r) -> r
withProObj @a @b Ob (ProObj BOOL p a b) => r
r = case forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @b of
    Yes p a b
_ -> r
Ob (ProObj BOOL p a b) => r
r
    Decision p a b (Holds p a b)
No -> r
Ob (ProObj BOOL p a b) => r
r
  underlying :: forall (a :: k) (b :: j). p a b -> Unit ~> ProObj BOOL p a b
underlying p a b
p = p a b
-> ((Holds p a b ~ 'TRU, Ob a, Ob b) =>
    Booleans 'TRU (Holds p a b))
-> Booleans 'TRU (Holds p a b)
forall (a :: k) (b :: j) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds p a b
p Booleans 'TRU 'TRU
Booleans 'TRU (Holds p a b)
(Holds p a b ~ 'TRU, Ob a, Ob b) => Booleans 'TRU (Holds p a b)
Tru
  enriched :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
(Unit ~> ProObj BOOL p a b) -> p a b
enriched @a @b Unit ~> ProObj BOOL p a b
f = case forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @b of
    Yes p a b
x -> p a b
x
    Decision p a b (Holds p a b)
No -> case Unit ~> ProObj BOOL p a b
f of {}
  rmap :: forall (a :: k) (b :: j) (c :: j).
(Ob a, Ob b, Ob c) =>
(HomObj BOOL b c ** ProObj BOOL p a b) ~> ProObj BOOL p a c
rmap @a @b @c = case (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> j) (a :: j) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @(Hom j) @b @c, forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @b) of
    (Yes b ~> c
g, Yes p a b
x) -> p a c
-> ((Holds p a c ~ 'TRU, Ob a, Ob c) =>
    Booleans 'TRU (Holds p a c))
-> Booleans 'TRU (Holds p a c)
forall (a :: k) (b :: j) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds ((b ~> c) -> p a b -> p a c
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
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
g p a b
x) Booleans 'TRU 'TRU
Booleans 'TRU (Holds p a c)
(Holds p a c ~ 'TRU, Ob a, Ob c) => Booleans 'TRU (Holds p a c)
Tru
    (Decision (Hom j) b c (Holds (Hom j) b c)
No, Decision p a b (Holds p a b)
_) -> Decision p a c (Holds p a c) -> Booleans 'FLS (Holds p a c)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (h :: BOOL).
Decision p a b h -> Booleans 'FLS h
fromFls (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @c)
    (Yes b ~> c
_, Decision p a b (Holds p a b)
No) -> Decision p a c (Holds p a c) -> Booleans 'FLS (Holds p a c)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (h :: BOOL).
Decision p a b h -> Booleans 'FLS h
fromFls (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @c)
  lmap :: forall (a :: k) (b :: j) (c :: k).
(Ob a, Ob b, Ob c) =>
(HomObj BOOL c a ** ProObj BOOL p a b) ~> ProObj BOOL p c b
lmap @a @b @c = case (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: k +-> k) (a :: k) (b :: k).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @(Hom k) @c @a, forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @b) of
    (Yes c ~> a
g, Yes p a b
x) -> p c b
-> ((Holds p c b ~ 'TRU, Ob c, Ob b) =>
    Booleans 'TRU (Holds p c b))
-> Booleans 'TRU (Holds p c b)
forall (a :: k) (b :: j) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds ((c ~> a) -> p a b -> p c b
forall (c :: k) (a :: k) (b :: j). (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
g p a b
x) Booleans 'TRU 'TRU
Booleans 'TRU (Holds p c b)
(Holds p c b ~ 'TRU, Ob c, Ob b) => Booleans 'TRU (Holds p c b)
Tru
    (Decision (Hom k) c a (Holds (Hom k) c a)
No, Decision p a b (Holds p a b)
_) -> Decision p c b (Holds p c b) -> Booleans 'FLS (Holds p c b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (h :: BOOL).
Decision p a b h -> Booleans 'FLS h
fromFls (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @c @b)
    (Yes c ~> a
_, Decision p a b (Holds p a b)
No) -> Decision p c b (Holds p c b) -> Booleans 'FLS (Holds p c b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (h :: BOOL).
Decision p a b h -> Booleans 'FLS h
fromFls (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @c @b)

-- | @FLS@ is initial, and a decision tells us which object we are aiming at.
fromFls :: Decision p a b h -> Booleans FLS h
fromFls :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (h :: BOOL).
Decision p a b h -> Booleans 'FLS h
fromFls (Yes p a b
_) = Booleans 'FLS h
Booleans 'FLS 'TRU
F2T
fromFls Decision p a b h
No = Booleans 'FLS h
Booleans 'FLS 'FLS
Fls

-- | __A finitary profunctor is a profunctor enriched in finite sets.__ The hom-object is the
-- hom-set itself, which 'Elt' makes an object of 'FINHASK' out of nothing but the numbering, and the
-- whiskerings are the two 'dimap's.
instance (Finitary p, LocallyFinite j, LocallyFinite k) => EnrichedProfunctor FINHASK (p :: j +-> k) where
  type ProObj FINHASK p a b = FH (Elt p a b)
  withProObj :: forall (a :: k) (b :: j) r.
(Ob a, Ob b) =>
(Ob (ProObj FINHASK p a b) => r) -> r
withProObj Ob (ProObj FINHASK p a b) => r
r = r
Ob (ProObj FINHASK p a b) => r
r
  underlying :: forall (a :: k) (b :: j). p a b -> Unit ~> ProObj FINHASK p a b
underlying p a b
x = (() -> Elt p a b) -> FinHask (FH ()) (FH (Elt p a b))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
F.arr (\() -> p a b -> Elt p a b
forall j k (p :: j +-> k) (a :: k) (b :: j). p a b -> Elt p a b
Elt p a b
x) ((Ob a, Ob b) => FinHask (FH ()) (FH (Elt p a b)))
-> p a b -> FinHask (FH ()) (FH (Elt p a b))
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
x
  enriched :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
(Unit ~> ProObj FINHASK p a b) -> p a b
enriched Unit ~> ProObj FINHASK p a b
f = Elt p a b -> p a b
forall j k (p :: j +-> k) (a :: k) (b :: j). Elt p a b -> p a b
unElt (Unit ~> ProObj FINHASK p a b
FinHask (FH ()) (FH (Elt p a b))
f FinHask (FH ()) (FH (Elt p a b))
-> UN FH (FH ()) -> UN FH (FH (Elt p a b))
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
F.! ())
  rmap :: forall (a :: k) (b :: j) (c :: j).
(Ob a, Ob b, Ob c) =>
(HomObj FINHASK b c ** ProObj FINHASK p a b)
~> ProObj FINHASK p a c
rmap @a = ((Elt (~>) b c, Elt p a b) -> Elt p a c)
-> FinHask (FH (Elt (~>) b c, Elt p a b)) (FH (Elt p a c))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
F.arr \(Elt b ~> c
g, Elt p a b
x) -> p a c -> Elt p a c
forall j k (p :: j +-> k) (a :: k) (b :: j). p a b -> Elt p a b
Elt ((a ~> a) -> (b ~> c) -> p a b -> p a c
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
P.dimap (forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id @_ @a) b ~> c
g p a b
x)
  lmap :: forall (a :: k) (b :: j) (c :: k).
(Ob a, Ob b, Ob c) =>
(HomObj FINHASK c a ** ProObj FINHASK p a b)
~> ProObj FINHASK p c b
lmap @_ @b = ((Elt (~>) c a, Elt p a b) -> Elt p c b)
-> FinHask (FH (Elt (~>) c a, Elt p a b)) (FH (Elt p c b))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
F.arr \(Elt c ~> a
g, Elt p a b
x) -> p c b -> Elt p c b
forall j k (p :: j +-> k) (a :: k) (b :: j). p a b -> Elt p a b
Elt ((c ~> a) -> (b ~> b) -> p a b -> p c b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
P.dimap c ~> a
g (forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: CAT j) (a :: j). (Promonad p, Ob a) => p a a
id @_ @b) p a b
x)

-- | The category of profunctors is enriched in itself: the hom-object is the internal hom
-- @p ':~>:' q@, an element of it is a natural transformation, and composition is the internal one.
-- Cartesian closed, hence the 'PROD' wrapper (@j '+->' k@\'s own tensor is Day convolution).
--
-- This self-enrichment is written the generic way, from 'HomSelf' and friends. Those apply to any
-- 'Closed' 'SymMonoidal' kind that has no enrichment instance of its own covering its
-- hom-profunctor.
instance (CategoryOf j, CategoryOf k) => EnrichedProfunctor (PROD (j +-> k)) (Prod (Prof :: CAT (j +-> k))) where
  type ProObj (PROD (j +-> k)) (Prod (Prof :: CAT (j +-> k))) p q = HomSelf p q
  withProObj :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) r.
(Ob a, Ob b) =>
(Ob (ProObj (PROD (j +-> k)) (Prod Prof) a b) => r) -> r
withProObj Ob (ProObj (PROD (j +-> k)) (Prod Prof) a b) => r
r = r
Ob (ProObj (PROD (j +-> k)) (Prod Prof) a b) => r
r
  underlying :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)).
Prod Prof a b -> Unit ~> ProObj (PROD (j +-> k)) (Prod Prof) a b
underlying = (a ~> b) -> Unit ~> HomSelf a b
Prod Prof a b -> Unit ~> ProObj (PROD (j +-> k)) (Prod Prof) a b
forall k (a :: k) (b :: k).
Closed k =>
(a ~> b) -> Unit ~> HomSelf a b
underlyingSelf
  enriched :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)).
(Ob a, Ob b) =>
(Unit ~> ProObj (PROD (j +-> k)) (Prod Prof) a b) -> Prod Prof a b
enriched = (Unit ~> HomSelf (PR (UN PR a)) (PR (UN PR b)))
-> PR (UN PR a) ~> PR (UN PR b)
(Unit ~> ProObj (PROD (j +-> k)) (Prod Prof) a b) -> Prod Prof a b
forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
(Unit ~> HomSelf a b) -> a ~> b
enrichedSelf
  rmap :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k))
       (c :: PROD (j +-> k)).
(Ob a, Ob b, Ob c) =>
(HomObj (PROD (j +-> k)) b c
 ** ProObj (PROD (j +-> k)) (Prod Prof) a b)
~> ProObj (PROD (j +-> k)) (Prod Prof) a c
rmap = (HomSelf (PR (UN PR b)) (PR (UN PR c))
 ** HomSelf (PR (UN PR a)) (PR (UN PR b)))
~> HomSelf (PR (UN PR a)) (PR (UN PR c))
(ProObj (PROD (j +-> k)) (Hom (PROD (j +-> k))) b c
 ** ProObj (PROD (j +-> k)) (Prod Prof) a b)
~> ProObj (PROD (j +-> k)) (Prod Prof) 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
compSelf
  lmap :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k))
       (c :: PROD (j +-> k)).
(Ob a, Ob b, Ob c) =>
(HomObj (PROD (j +-> k)) c a
 ** ProObj (PROD (j +-> k)) (Prod Prof) a b)
~> ProObj (PROD (j +-> k)) (Prod Prof) c b
lmap = (HomSelf (PR (UN PR a)) (PR (UN PR b))
 ** HomSelf (PR (UN PR c)) (PR (UN PR a)))
~> HomSelf (PR (UN PR c)) (PR (UN PR b))
Prod
  Prof
  (PR
     ((UN PR (PR (UN PR a)) :~>: UN PR b)
      :*: (UN PR c :~>: UN PR (PR (UN PR a)))))
  (PR (UN PR c :~>: UN PR b))
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 Prod
  Prof
  (PR
     ((UN PR (PR (UN PR a)) :~>: UN PR b)
      :*: (UN PR c :~>: UN PR (PR (UN PR a)))))
  (PR (UN PR c :~>: UN PR b))
-> Prod
     Prof
     (PR ((UN PR c :~>: UN PR a) :*: (UN PR a :~>: UN PR b)))
     (PR
        ((UN PR (PR (UN PR a)) :~>: UN PR b)
         :*: (UN PR c :~>: UN PR (PR (UN PR a)))))
-> Prod
     Prof
     (PR ((UN PR c :~>: UN PR a) :*: (UN PR a :~>: UN PR b)))
     (PR (UN PR c :~>: UN PR b))
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: PROD (j +-> k)) (c :: PROD (j +-> k))
       (a :: PROD (j +-> k)).
Prod Prof b c -> Prod Prof a b -> Prod Prof a c
. (PR (UN PR c :~>: UN PR a) ** PR (UN PR a :~>: UN PR b))
~> (PR (UN PR a :~>: UN PR b) ** PR (UN PR c :~>: UN PR a))
Prod
  Prof
  (PR ((UN PR c :~>: UN PR a) :*: (UN PR a :~>: UN PR b)))
  (PR
     ((UN PR (PR (UN PR a)) :~>: UN PR b)
      :*: (UN PR c :~>: UN PR (PR (UN PR a)))))
forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap

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 (Hom k) (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 (Hom k) (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 (Hom j) (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 (Hom j) (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)

-- | A generalized arrow of an enriched category. If @k@ is both powered and copowered, this is an adjunction.
type GenArrow :: OPPOSITE v -> k +-> k
data GenArrow n a b where
  GenArrow :: (Ob a, Ob b) => n ~> HomObj v a b -> GenArrow (OP n) a b

instance (Ob (n :: v), Enriched v k, CategoryOf k) => Profunctor (GenArrow (OP n) :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> GenArrow (OP n) a b -> GenArrow (OP n) c d
dimap @c @a @b @d c ~> a
l b ~> d
r (GenArrow n ~> HomObj v a b
f) =
    (n ~> HomObj v c d) -> GenArrow (OP n) c d
forall {k} (a :: k) (b :: k) v (n :: v).
(Ob a, Ob b) =>
(n ~> HomObj v a b) -> GenArrow (OP n) a b
GenArrow
      ( let g :: n ~> ProObj v (Hom k) c b
g = forall 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
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 @v @c @a @b ((HomObj v a b ** HomObj v c a) ~> ProObj v (Hom k) c b)
-> (n ~> (HomObj v a b ** HomObj v c a))
-> n ~> ProObj v (Hom k) c b
forall (b :: v) (c :: v) (a :: v). (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
. (Unit ~> HomObj v c a)
-> HomObj v a b ~> (HomObj v a b ** HomObj v c a)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (a ** b)
rightUnitorInvWith (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 :: k +-> k) (a :: k) (b :: k).
EnrichedProfunctor v p =>
p a b -> Unit ~> ProObj v p a b
underlying @v c ~> a
l) (HomObj v a b ~> (HomObj v a b ** HomObj v c a))
-> (n ~> HomObj v a b) -> n ~> (HomObj v a b ** HomObj v c a)
forall (b :: v) (c :: v) (a :: v). (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
. n ~> HomObj v a b
n ~> HomObj v a b
f
        in forall 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
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 @v @c @b @d ((HomObj v b d ** ProObj v (Hom k) c b) ~> HomObj v c d)
-> (n ~> (HomObj v b d ** ProObj v (Hom k) c b))
-> n ~> HomObj v c d
forall (b :: v) (c :: v) (a :: v). (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
. (Unit ~> HomObj v b d)
-> ProObj v (Hom k) c b ~> (HomObj v b d ** ProObj v (Hom k) c b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (b ** a)
leftUnitorInvWith (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 :: k +-> k) (a :: k) (b :: k).
EnrichedProfunctor v p =>
p a b -> Unit ~> ProObj v p a b
underlying @v b ~> d
r) (ProObj v (Hom k) c b ~> (HomObj v b d ** ProObj v (Hom k) c b))
-> (n ~> ProObj v (Hom k) c b)
-> n ~> (HomObj v b d ** ProObj v (Hom k) c b)
forall (b :: v) (c :: v) (a :: v). (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
. n ~> ProObj v (Hom k) c b
g ((Ob n, Ob (ProObj v (Hom k) c b)) => n ~> HomObj v c d)
-> (n ~> ProObj v (Hom k) c b) -> n ~> HomObj v c d
forall (a :: v) (b :: v) 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
\\ n ~> ProObj v (Hom k) c b
g
      )
      ((Ob n, Ob (HomObj v a b)) => GenArrow (OP n) c d)
-> (n ~> HomObj v a b) -> GenArrow (OP n) c d
forall (a :: v) (b :: v) 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
\\ n ~> HomObj v a b
n ~> HomObj v a b
f
      ((Ob c, Ob a) => GenArrow (OP n) c d)
-> (c ~> a) -> GenArrow (OP n) c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c ~> a
l
      ((Ob b, Ob d) => GenArrow (OP n) c d)
-> (b ~> d) -> GenArrow (OP n) c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> d
r
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> GenArrow (OP n) a b -> r
\\ GenArrow n ~> HomObj v a b
f = r
(Ob n, Ob (HomObj v a b)) => r
(Ob a, Ob b) => r
r ((Ob n, Ob (HomObj v a b)) => r) -> (n ~> HomObj v a b) -> r
forall (a :: v) (b :: v) 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
\\ n ~> HomObj v a b
n ~> HomObj v a b
f