{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.Rel where

import Proarrow.Adjunction (Adjunction (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), src, (:~>), type (+->), Promonad (..))
import Proarrow.Preorder.ThinCategory (Discrete, ThinProfunctor (..), withEq)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Representable (Representable (..), trivialRep)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))

class (ThinProfunctor p, Discrete j, Discrete k) => Relation (p :: j +-> k)
instance (ThinProfunctor p, Discrete j, Discrete k) => Relation (p :: j +-> k)

type Converse :: (j +-> k) -> (k +-> j)
data Converse p a b where
  Converse :: p b a -> Converse p a b
instance (Relation p) => Profunctor (Converse p) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Converse p a b -> Converse p c d
dimap c ~> a
f b ~> d
g (Converse p b a
p) = (c ~> a) -> ((c ~ a) => Converse p c d) -> Converse p c d
forall (a :: k) (b :: k) r. (a ~> b) -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
DiscreteProfunctor p =>
p a b -> ((a ~ b) => r) -> r
withEq c ~> a
f ((b ~> d) -> ((b ~ d) => Converse p c d) -> Converse p c d
forall (a :: j) (b :: j) r. (a ~> b) -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
DiscreteProfunctor p =>
p a b -> ((a ~ b) => r) -> r
withEq b ~> d
g (p d c -> Converse p c d
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Converse p a b
Converse p b a
p d c
p))
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Converse p a b -> r
\\ Converse p b a
p = r
(Ob a, Ob b) => r
(Ob b, Ob a) => r
r ((Ob b, Ob a) => r) -> p b a -> r
forall (a :: j) (b :: k) 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 b a
p
instance (Relation p) => ThinProfunctor (Converse p) where
  type HasArrow (Converse p) a b = HasArrow p b a
  arr :: forall (a :: k) (b :: j).
(Ob a, Ob b, HasArrow (Converse p) a b) =>
Converse p a b
arr = p b a -> Converse p a b
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Converse p a b
Converse p b a
forall (a :: j) (b :: k). (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
  withArr :: forall (a :: k) (b :: j) r.
Converse p a b -> (HasArrow (Converse p) a b => r) -> r
withArr (Converse p b a
p) HasArrow (Converse p) a b => r
r = p b a -> (HasArrow p b a => r) -> r
forall (a :: j) (b :: k) 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 b a
p r
HasArrow p b a => r
HasArrow (Converse p) a b => r
r
instance (Relation p, Representable p) => Corepresentable (Converse p) where
  type (Converse p) %% a = p % a
  coindex :: forall (a :: k) (b :: j). Converse p a b -> (Converse p %% a) ~> b
coindex (Converse p b a
p) = (b ~> (p % a)) -> ((b ~ (p % a)) => (p % a) ~> b) -> (p % a) ~> b
forall (a :: j) (b :: j) r. (a ~> b) -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
DiscreteProfunctor p =>
p a b -> ((a ~ b) => r) -> r
withEq (p b a -> b ~> (p % a)
forall (a :: j) (b :: k). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p b a
p) (p b a -> Obj b
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src p b a
p)
  cotabulate :: forall (a :: k) (b :: j).
Ob a =>
((Converse p %% a) ~> b) -> Converse p a b
cotabulate (Converse p %% a) ~> b
f = ((p % a) ~> b)
-> (((p % a) ~ b) => Converse p a b) -> Converse p a b
forall (a :: j) (b :: j) r. (a ~> b) -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
DiscreteProfunctor p =>
p a b -> ((a ~ b) => r) -> r
withEq (Converse p %% a) ~> b
(p % a) ~> b
f (p b a -> Converse p a b
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Converse p a b
Converse ((b ~> (p % a)) -> p b a
forall (b :: k) (a :: j). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate b ~> (p % a)
(Converse p %% a) ~> b
f))
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (Converse p %% a) ~> (Converse p %% b)
corepMap a ~> b
f = (a ~> b) -> ((a ~ b) => (p % a) ~> (p % b)) -> (p % a) ~> (p % b)
forall (a :: k) (b :: k) r. (a ~> b) -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
DiscreteProfunctor p =>
p a b -> ((a ~ b) => r) -> r
withEq a ~> b
f (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> j) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p ((b ~> b) -> b ~> b
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src a ~> b
b ~> b
f))

asImplication
  :: forall a b p q r. (Relation p, Relation q) => p :~> q -> (Ob a, Ob b, HasArrow p a b) => ((HasArrow q a b) => r) -> r
asImplication :: forall {k} {j} (a :: k) (b :: j) (p :: j +-> k) (q :: j +-> k) r.
(Relation p, Relation q) =>
(p :~> q)
-> (Ob a, Ob b, HasArrow p a b) => (HasArrow q a b => r) -> r
asImplication p :~> q
n = q a b -> (HasArrow q a b => r) -> r
forall (a :: k) (b :: j) r. q a b -> (HasArrow q 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 -> q a b
p :~> q
n (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))

class (Relation p) => Functional p where
  isFunctional :: p :.: Converse p :~> (~>)

reprIsFunctional :: (Relation p, Representable p) => p :.: Converse p :~> (~>)
reprIsFunctional :: forall {j} {k1} (p :: j +-> k1).
(Relation p, Representable p) =>
(p :.: Converse p) :~> (~>)
reprIsFunctional (p a b
p :.: Converse p b b
p') = (a ~> (p % b)) -> ((a ~ (p % b)) => a ~> b) -> a ~> b
forall (a :: k1) (b :: k1) r. (a ~> b) -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
DiscreteProfunctor p =>
p a b -> ((a ~ b) => r) -> r
withEq (p a b -> a ~> (p % b)
forall (a :: k1) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p a b
p) ((b ~> a) -> ((b ~ a) => a ~> b) -> a ~> b
forall (a :: k1) (b :: k1) r. (a ~> b) -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
DiscreteProfunctor p =>
p a b -> ((a ~ b) => r) -> r
withEq (p b b -> b ~> (p % b)
forall (a :: k1) (b :: j). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p b b
p') (p a b -> Obj a
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src p a b
p))

class (Relation p) => Total p where
  isTotal :: (~>) :~> Converse p :.: p

reprIsTotal :: (Relation p, Representable p) => (~>) :~> Converse p :.: p
reprIsTotal :: forall {k1} {j} (p :: k1 +-> j).
(Relation p, Representable p) =>
(~>) :~> (Converse p :.: p)
reprIsTotal a ~> b
f = (a ~> b)
-> ((a ~ b) => (:.:) (Converse p) p a b)
-> (:.:) (Converse p) p a b
forall (a :: k1) (b :: k1) r. (a ~> b) -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
DiscreteProfunctor p =>
p a b -> ((a ~ b) => r) -> r
withEq a ~> b
f (p (p % b) a -> Converse p a (p % b)
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Converse p a b
Converse p (p % a) a
p (p % b) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep Converse p a (p % b) -> p (p % b) b -> (:.:) (Converse p) p a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p (p % b) b
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep) ((Ob a, Ob b) => (:.:) (Converse p) p a b)
-> (a ~> b) -> (:.:) (Converse p) p a b
forall (a :: k1) (b :: k1) 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
\\ a ~> b
f

class (Relation p) => Injective p where
  isInjective :: Converse p :.: p :~> (~>)

class (Relation p) => Surjective p where
  isSurjective :: (~>) :~> p :.: Converse p

adjToConverse :: forall p q. (Relation p, Relation q, Adjunction p q) => q :~> Converse p
adjToConverse :: forall {j} {k} (p :: j +-> k) (q :: k +-> j).
(Relation p, Relation q, Adjunction p q) =>
q :~> Converse p
adjToConverse q a b
q = p b a -> Converse p a b
forall {j} {k} (p :: j +-> k) (b :: k) (a :: j).
p b a -> Converse p a b
Converse (case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: j +-> k) (q :: k +-> j) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit @p @q of q a b
_ :.: p b a
p -> (b ~> b) -> ((b ~ b) => p b a) -> p b a
forall (a :: k) (b :: k) r. (a ~> b) -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
DiscreteProfunctor p =>
p a b -> ((a ~ b) => r) -> r
withEq ((:.:) p q b b -> b ~> b
(p :.: q) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Adjunction p q =>
(p :.: q) :~> (~>)
counit (p b a
p p b a -> q a b -> (:.:) p q b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: q a b
q)) p b a
p b a
(b ~ b) => p b a
p) ((Ob a, Ob b) => Converse p a b) -> q a b -> Converse p a b
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> q 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
\\ q a b
q

adjFromConverse :: forall p q. (Relation p, Relation q, Adjunction p q) => Converse p :~> q
adjFromConverse :: forall {k} {k1} (p :: k +-> k1) (q :: k1 +-> k).
(Relation p, Relation q, Adjunction p q) =>
Converse p :~> q
adjFromConverse (Converse @_ @_ @a p b a
p) = (case forall {j} {k} (p :: j +-> k) (q :: k +-> j) (a :: j).
(Adjunction p q, Ob a) =>
(:.:) q p a a
forall (p :: k +-> k1) (q :: k1 +-> k) (a :: k).
(Adjunction p q, Ob a) =>
(:.:) q p a a
unit @p @q @a of q a b
q :.: p b a
_ -> (b ~> b) -> ((b ~ b) => q a b) -> q a b
forall (a :: k1) (b :: k1) r. (a ~> b) -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
DiscreteProfunctor p =>
p a b -> ((a ~ b) => r) -> r
withEq ((:.:) p q b b -> b ~> b
(p :.: q) :~> (~>)
forall {j} {k} (p :: j +-> k) (q :: k +-> j).
Adjunction p q =>
(p :.: q) :~> (~>)
counit (p b a
p p b a -> q a b -> (:.:) p q b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: q a b
q)) q a b
q a b
(b ~ b) => q a b
q) ((Ob b, Ob a) => q a b) -> p b a -> q a b
forall (a :: k1) (b :: k) 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 b a
p

class (Relation p, Promonad p) => Preorder p
instance (Relation p, Promonad p) => Preorder p