-- | __Sieves__: a @'Sieve' a b@ says which arrows into @a@ and out of @b@ are in, closed under
-- composition on both sides. Sieves are the subobjects of the representable at @a@\/@b@, so they are
-- the truth values of a category of profunctors, and
-- "Proarrow.Category.Enriched.Finitary" makes them the
-- 'Proarrow.Category.Topos.HasSubobjectClassifier' of the finitary ones.
module Proarrow.Profunctor.Instance.Sieve where

import Prelude (Bool)

import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (//), type (+->))

type Sieve :: forall {j} {k}. j +-> k
data Sieve a b where
  Sieve :: (Ob a, Ob b) => (forall c d. c ~> a -> b ~> d -> Bool) -> Sieve a b

instance (CategoryOf j, CategoryOf k) => Profunctor (Sieve :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Sieve a b -> Sieve c d
dimap c ~> a
l b ~> d
r (Sieve forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool
s) = c ~> a
l (c ~> a) -> ((Ob c, Ob a) => Sieve c d) -> Sieve 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) => Sieve c d) -> Sieve 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) -> Bool)
-> Sieve c d
forall {k} {j} (a :: k) (b :: j).
(Ob a, Ob b) =>
(forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool)
-> Sieve a b
Sieve \c ~> c
g d ~> d
h -> (c ~> a) -> (b ~> d) -> Bool
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool
s (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
g) (d ~> d
h (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)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Sieve a b -> r
\\ Sieve{} = r
(Ob a, Ob b) => r
r