{-# OPTIONS_GHC -Wno-orphans #-}

-- | The internal hom of the category of profunctors under the /product/: a @(p ':~>:' q) a b@ is a
-- natural family of maps @p c d -> q c d@ available at @a@\/@b@, making @'PROD' (j +-> k)@ 'Closed'.
-- @j +-> k@ itself is 'Closed' too, but for Day convolution and with a different hom (see
-- "Proarrow.Profunctor.Instance.Day"). The 'PROD' wrapper keeps the two apart.
module Proarrow.Profunctor.Instance.Exponential where

import Proarrow.Category.Enriched.Thin
  ( DecidableProfunctor (..)
  , Decision (..)
  , Discrete
  , ThinProfunctor (..)
  , noArrow
  , withEq
  )
import Proarrow.Category.Instance.Bool (BoolLeq)
import Proarrow.Category.Instance.Constraint (reifyExp, (:=>) (..), type (:-) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (IsObProd, SUBCAT (..), Sub (..))
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Core (CategoryOf (..), OB, Profunctor (..), Promonad (..), UN, (//), type (+->))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts, PROD (..), Prod (..))
import Proarrow.Limit.Terminal (HasTerminalObject)
import Proarrow.Profunctor.Instance.Product ((:*:) (..))

data (p :~>: q) a b where
  Exp :: (Ob a, Ob b) => (forall c d. c ~> a -> b ~> d -> p c d -> q c d) -> (p :~>: q) a b

instance (Profunctor p, Profunctor q) => Profunctor (p :~>: q) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> (:~>:) p q a b -> (:~>:) p q c d
dimap c ~> a
l b ~> d
r (Exp forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d
f) = c ~> a
l (c ~> a) -> ((Ob c, Ob a) => (:~>:) p q c d) -> (:~>:) p q c d
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// b ~> d
r (b ~> d) -> ((Ob b, Ob d) => (:~>:) p q c d) -> (:~>:) p q c d
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (c :: k) (d :: j). (c ~> c) -> (d ~> d) -> p c d -> q c d)
-> (:~>:) p q c d
forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type)
       (q :: k -> k -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> c
ca d ~> d
bd p c d
p -> (c ~> a) -> (b ~> d) -> p c d -> q c d
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d
f (c ~> a
l (c ~> a) -> (c ~> c) -> c ~> a
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
. c ~> c
ca) (d ~> d
bd (d ~> d) -> (b ~> d) -> b ~> d
forall (b :: j) (c :: j) (a :: j). (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
. b ~> d
r) p c d
p
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> (:~>:) p q a b -> r
\\ Exp{} = r
(Ob a, Ob b) => r
r

instance (CategoryOf j, CategoryOf k) => Closed (PROD (j +-> k)) where
  type p ~~> q = PR (UN PR p :~>: UN PR q)
  withObExp :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k))
       (c :: PROD (j +-> k)).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry (Prod (Prof (UN PR a :*: UN PR b) :~> b1
n)) = Prof (UN PR a) (UN PR b :~>: b1)
-> Prod Prof (PR (UN PR a)) (PR (UN PR b :~>: b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod ((UN PR a :~> (UN PR b :~>: b1)) -> Prof (UN PR a) (UN PR b :~>: b1)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \UN PR a a b
p -> UN PR a a b
p UN PR a a b
-> ((Ob a, Ob b) => (:~>:) (UN PR b) b1 a b)
-> (:~>:) (UN PR b) b1 a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (c :: k) (d :: j).
 (c ~> a) -> (b ~> d) -> UN PR b c d -> b1 c d)
-> (:~>:) (UN PR b) b1 a b
forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type)
       (q :: k -> k -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd UN PR b c d
q -> (:*:) (UN PR a) (UN PR b) c d -> b1 c d
(UN PR a :*: UN PR b) :~> b1
n ((c ~> a) -> (b ~> d) -> UN PR a a b -> UN PR a c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> UN PR a a b -> UN PR a 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
dimap c ~> a
ca b ~> d
bd UN PR a a b
p UN PR a c d -> UN PR b c d -> (:*:) (UN PR a) (UN PR b) c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: UN PR b c d
q))
  apply :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k)).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = Prof ((UN PR a :~>: UN PR b) :*: UN PR a) (UN PR b)
-> Prod
     Prof (PR ((UN PR a :~>: UN PR b) :*: UN PR a)) (PR (UN PR b))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod ((((UN PR a :~>: UN PR b) :*: UN PR a) :~> UN PR b)
-> Prof ((UN PR a :~>: UN PR b) :*: UN PR a) (UN PR b)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Exp forall (c :: k) (d :: j).
(c ~> a) -> (b ~> d) -> UN PR a c d -> UN PR b c d
f :*: UN PR a a b
q) -> (a ~> a) -> (b ~> b) -> UN PR a a b -> UN PR b a b
forall (c :: k) (d :: j).
(c ~> a) -> (b ~> d) -> UN PR a c d -> UN PR b c d
f a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id UN PR a a b
q ((Ob a, Ob b) => UN PR b a b) -> UN PR a a b -> UN PR b a b
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> UN PR a 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
\\ UN PR a a b
q)
  Prod (Prof a1 :~> b1
m) ^^^ :: forall (a :: PROD (j +-> k)) (b :: PROD (j +-> k))
       (x :: PROD (j +-> k)) (y :: PROD (j +-> k)).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Prod (Prof a1 :~> b1
n) = Prof (b1 :~>: a1) (a1 :~>: b1)
-> Prod Prof (PR (b1 :~>: a1)) (PR (a1 :~>: b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod (((b1 :~>: a1) :~> (a1 :~>: b1)) -> Prof (b1 :~>: a1) (a1 :~>: b1)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Exp forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
f) -> (forall (c :: k) (d :: j).
 (c ~> a) -> (b ~> d) -> a1 c d -> b1 c d)
-> (:~>:) a1 b1 a b
forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type)
       (q :: k -> k -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd a1 c d
p -> a1 c d -> b1 c d
a1 :~> b1
m ((c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
f c ~> a
ca b ~> d
bd (a1 c d -> b1 c d
a1 :~> b1
n a1 c d
p)))

-- | That a full subcategory of the profunctors contains the internal homs of its objects, as a
-- class with a single instance, so that it can be the head of the quantified constraint below.
-- 'Proarrow.Category.Instance.Sub.IsObProd' has the same shape for the product.
class (ob (p :~>: q)) => IsObExp (ob :: OB (j +-> k)) p q

instance (ob (p :~>: q)) => IsObExp ob p q

-- | And then the subcategory is closed, with the ambient exponential and nothing of its own,
-- just as its products are the ambient ones. @'Proarrow.Category.Enriched.Finitary.Topos.FINITARY'
-- j k@ is one instance, 'Proarrow.Category.Enriched.Finitary.Sheaf.SHEAVES' another. For the
-- first, a hom-set of natural transformations is finitary. For the second, an internal hom into a
-- sheaf is a sheaf.
instance
  ( CategoryOf j
  , CategoryOf k
  , HasTerminalObject (SUBCAT ob)
  , HasBinaryProducts (SUBCAT ob)
  , -- the product one again, as a constraint: 'apply' needs @ob@ of a product whose left factor is
    -- an internal hom, which no @'Ob' _@ in scope mentions
    forall p q. (ob p, ob q) => IsObProd ob p q
  , forall p q. (ob p, ob q) => IsObExp ob p q
  )
  => Closed (PROD (SUBCAT (ob :: OB (j +-> k))))
  where
  type p ~~> q = PR (SUB (UN SUB (UN PR p) :~>: UN SUB (UN PR q)))
  withObExp :: forall (a :: PROD (SUBCAT ob)) (b :: PROD (SUBCAT ob)) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: PROD (SUBCAT ob)) (b :: PROD (SUBCAT ob))
       (c :: PROD (SUBCAT ob)).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry (Prod (Sub (Prof (UN SUB (UN PR a) :*: UN SUB (UN PR b)) :~> b1
n))) = Sub Prof (SUB (UN SUB (UN PR a))) (SUB (UN SUB (UN PR b) :~>: b1))
-> Prod
     (Sub Prof)
     (PR (SUB (UN SUB (UN PR a))))
     (PR (SUB (UN SUB (UN PR b) :~>: b1)))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod (Prof (UN SUB (UN PR a)) (UN SUB (UN PR b) :~>: b1)
-> Sub
     Prof (SUB (UN SUB (UN PR a))) (SUB (UN SUB (UN PR b) :~>: b1))
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 ((UN SUB (UN PR a) :~> (UN SUB (UN PR b) :~>: b1))
-> Prof (UN SUB (UN PR a)) (UN SUB (UN PR b) :~>: b1)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \UN SUB (UN PR a) a b
p -> UN SUB (UN PR a) a b
p UN SUB (UN PR a) a b
-> ((Ob a, Ob b) => (:~>:) (UN SUB (UN PR b)) b1 a b)
-> (:~>:) (UN SUB (UN PR b)) b1 a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (c :: k) (d :: j).
 (c ~> a) -> (b ~> d) -> UN SUB (UN PR b) c d -> b1 c d)
-> (:~>:) (UN SUB (UN PR b)) b1 a b
forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type)
       (q :: k -> k -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd UN SUB (UN PR b) c d
q -> (:*:) (UN SUB (UN PR a)) (UN SUB (UN PR b)) c d -> b1 c d
(UN SUB (UN PR a) :*: UN SUB (UN PR b)) :~> b1
n ((c ~> a)
-> (b ~> d) -> UN SUB (UN PR a) a b -> UN SUB (UN PR a) c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> UN SUB (UN PR a) a b -> UN SUB (UN PR a) 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
dimap c ~> a
ca b ~> d
bd UN SUB (UN PR a) a b
p UN SUB (UN PR a) c d
-> UN SUB (UN PR b) c d
-> (:*:) (UN SUB (UN PR a)) (UN SUB (UN PR b)) c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: UN SUB (UN PR b) c d
q)))
  apply :: forall (a :: PROD (SUBCAT ob)) (b :: PROD (SUBCAT ob)).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = Sub
  Prof
  (SUB
     ((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a)))
  (SUB (UN SUB (UN PR b)))
-> Prod
     (Sub Prof)
     (PR
        (SUB
           ((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a))))
     (PR (SUB (UN SUB (UN PR b))))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod (Prof
  ((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a))
  (UN SUB (UN PR b))
-> Sub
     Prof
     (SUB
        ((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a)))
     (SUB (UN SUB (UN PR b)))
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 ((((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a))
 :~> UN SUB (UN PR b))
-> Prof
     ((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a))
     (UN SUB (UN PR b))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Exp forall (c :: k) (d :: j).
(c ~> a)
-> (b ~> d) -> UN SUB (UN PR a) c d -> UN SUB (UN PR b) c d
f :*: UN SUB (UN PR a) a b
q) -> (a ~> a)
-> (b ~> b) -> UN SUB (UN PR a) a b -> UN SUB (UN PR b) a b
forall (c :: k) (d :: j).
(c ~> a)
-> (b ~> d) -> UN SUB (UN PR a) c d -> UN SUB (UN PR b) c d
f a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id UN SUB (UN PR a) a b
q ((Ob a, Ob b) => UN SUB (UN PR b) a b)
-> UN SUB (UN PR a) a b -> UN SUB (UN PR b) a b
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> UN SUB (UN PR a) 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
\\ UN SUB (UN PR a) a b
q))
  Prod (Sub (Prof a1 :~> b1
m)) ^^^ :: forall (a :: PROD (SUBCAT ob)) (b :: PROD (SUBCAT ob))
       (x :: PROD (SUBCAT ob)) (y :: PROD (SUBCAT ob)).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Prod (Sub (Prof a1 :~> b1
n)) = Sub Prof (SUB (b1 :~>: a1)) (SUB (a1 :~>: b1))
-> Prod (Sub Prof) (PR (SUB (b1 :~>: a1))) (PR (SUB (a1 :~>: b1)))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod (Prof (b1 :~>: a1) (a1 :~>: b1)
-> Sub Prof (SUB (b1 :~>: a1)) (SUB (a1 :~>: b1))
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 (((b1 :~>: a1) :~> (a1 :~>: b1)) -> Prof (b1 :~>: a1) (a1 :~>: b1)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Exp forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
f) -> (forall (c :: k) (d :: j).
 (c ~> a) -> (b ~> d) -> a1 c d -> b1 c d)
-> (:~>:) a1 b1 a b
forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type)
       (q :: k -> k -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd a1 c d
p -> a1 c d -> b1 c d
a1 :~> b1
m ((c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
f c ~> a
ca b ~> d
bd (a1 c d -> b1 c d
a1 :~> b1
n a1 c d
p))))

instance (ThinProfunctor p, ThinProfunctor q, Discrete j, Discrete k) => ThinProfunctor (p :~>: q :: j +-> k) where
  type HasArrow (p :~>: q) a b = (HasArrow p a b :=> HasArrow q a b)
  arr :: forall (a :: k) (b :: j).
(Ob a, Ob b, HasArrow (p :~>: q) a b) =>
(:~>:) p q a b
arr @a @b = (forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type)
       (q :: k -> k -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd p c d
p -> (c ~> a) -> ((c ~ a) => q c d) -> q c d
forall (a :: k) (b :: k) r. (a ~> b) -> ((a ~ b) => r) -> r
forall k (a :: k) (b :: k) r.
Discrete k =>
(a ~> b) -> ((a ~ b) => r) -> r
withEq c ~> a
ca ((b ~> d) -> ((b ~ d) => q c d) -> q c d
forall (a :: j) (b :: j) r. (a ~> b) -> ((a ~ b) => r) -> r
forall k (a :: k) (b :: k) r.
Discrete k =>
(a ~> b) -> ((a ~ b) => r) -> r
withEq b ~> d
bd (p c d -> ((HasArrow p c d, Ob c, Ob d) => q c d) -> q c d
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 c d
p ((CNSTRNT (HasArrow p a b) :- CNSTRNT (HasArrow q a b))
-> forall r. HasArrow p a b => (HasArrow q a b => r) -> r
forall (a :: Constraint) (b :: Constraint).
(CNSTRNT a :- CNSTRNT b) -> forall r. a => (b => r) -> r
unEntails (forall (b :: Constraint) (c :: Constraint).
(b :=> c) =>
CNSTRNT b :- CNSTRNT c
entails @(HasArrow p a b) @(HasArrow q a b)) q c d
HasArrow q a b => q c d
forall (a :: k) (b :: j). (Ob a, Ob b, HasArrow q a b) => q 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)))
  withArr :: forall (a :: k) (b :: j) r.
(:~>:) p q a b -> ((HasArrow (p :~>: q) a b, Ob a, Ob b) => r) -> r
withArr @a @b (Exp forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d
f) (HasArrow (p :~>: q) a b, Ob a, Ob b) => r
r = (CNSTRNT (HasArrow p a b) :- CNSTRNT (HasArrow q a b))
-> ((HasArrow p a b :=> HasArrow q a b) => r) -> r
forall (b :: Constraint) (c :: Constraint) r.
(CNSTRNT b :- CNSTRNT c) -> ((b :=> c) => r) -> r
reifyExp (forall (a1 :: Constraint) (b1 :: Constraint).
(forall r. a1 => (b1 => r) -> r) -> CNSTRNT a1 :- CNSTRNT b1
Entails @(HasArrow p a b) @(HasArrow q a b) (\HasArrow q a b => r
r' -> q a b -> ((HasArrow q a b, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: j) r.
q a b -> ((HasArrow q 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 ((a ~> a) -> (b ~> b) -> p a b -> q a b
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d
f a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id 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) r
HasArrow q a b => r
(HasArrow q a b, Ob a, Ob b) => r
r')) r
(HasArrow (p :~>: q) a b, Ob a, Ob b) => r
(HasArrow p a b :=> HasArrow q a b) => r
r

-- | Implication, decided: the exponential holds unless @p@ holds and @q@ does not. Against @p@ an
-- arrow of @p@ is refuted by 'noArrow'.
instance
  (DecidableProfunctor p, DecidableProfunctor q, Discrete j, Discrete k)
  => DecidableProfunctor (p :~>: q :: j +-> k)
  where
  type Holds (p :~>: q) a b = BoolLeq (Holds p a b) (Holds q a b)
  decide :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
Decision (p :~>: q) a b (Holds (p :~>: q) a b)
decide @a @b = 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, 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 @q @a @b) of
    (Decision p a b (Holds p a b)
_, Yes q a b
y) -> (:~>:) p q a b -> Decision (p :~>: q) a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes ((forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type)
       (q :: k -> k -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd p c d
_ -> (c ~> a) -> ((c ~ a) => q c d) -> q c d
forall (a :: k) (b :: k) r. (a ~> b) -> ((a ~ b) => r) -> r
forall k (a :: k) (b :: k) r.
Discrete k =>
(a ~> b) -> ((a ~ b) => r) -> r
withEq c ~> a
ca ((b ~> d) -> ((b ~ d) => q c d) -> q c d
forall (a :: j) (b :: j) r. (a ~> b) -> ((a ~ b) => r) -> r
forall k (a :: k) (b :: k) r.
Discrete k =>
(a ~> b) -> ((a ~ b) => r) -> r
withEq b ~> d
bd q a b
q c d
(b ~ d) => q c d
y))
    (Decision p a b (Holds p a b)
No, Decision q a b (Holds q a b)
No) -> (:~>:) p q a b -> Decision (p :~>: q) a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes ((forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type)
       (q :: k -> k -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd p c d
x -> (c ~> a) -> ((c ~ a) => q c d) -> q c d
forall (a :: k) (b :: k) r. (a ~> b) -> ((a ~ b) => r) -> r
forall k (a :: k) (b :: k) r.
Discrete k =>
(a ~> b) -> ((a ~ b) => r) -> r
withEq c ~> a
ca ((b ~> d) -> ((b ~ d) => q c d) -> q c d
forall (a :: j) (b :: j) r. (a ~> b) -> ((a ~ b) => r) -> r
forall k (a :: k) (b :: k) r.
Discrete k =>
(a ~> b) -> ((a ~ b) => r) -> r
withEq b ~> d
bd (p c d -> q c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
(DecidableProfunctor p, Holds p a b ~ 'FLS) =>
p a b -> r
noArrow p c d
x)))
    (Yes p a b
_, Decision q a b (Holds q a b)
No) -> Decision (p :~>: q) a b 'FLS
Decision (p :~>: q) a b (Holds (p :~>: q) a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
  toHolds :: forall (a :: k) (b :: j) r.
(:~>:) p q a b
-> ((Holds (p :~>: q) a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds @a @b (Exp forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d
f) (Holds (p :~>: q) a b ~ 'TRU, Ob a, Ob 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
x -> q a b -> ((Holds q a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: j) r.
q a b -> ((Holds q 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 ((a ~> a) -> (b ~> b) -> p a b -> q a b
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d
f a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id p a b
x) r
(Holds q a b ~ 'TRU, Ob a, Ob b) => r
(Holds (p :~>: q) a b ~ 'TRU, Ob a, Ob b) => r
r
    Decision p a b (Holds p a b)
No -> r
(Holds (p :~>: q) a b ~ 'TRU, Ob a, Ob b) => r
r