{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

-- | Galois connections have the same properties as adjunctions defined over other categories:
--
--  \( \forall x, y : f \dashv g \Rightarrow f (x) \leq b \Leftrightarrow x \leq g (y) \)
--
--  \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \)
--
--  \( \forall x, y : x \leq y \Rightarrow g (x) \leq g (y) \)
--
--  \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \)
--
--  \( \forall x : f \dashv g \Rightarrow f \circ g (x) \leq x \)
--
--  \( \forall x : unit \circ unit (x) \sim unit (x) \)
--
--  \( \forall x : counit \circ counit (x) \sim counit (x) \)
--
--  \( \forall x : counit \circ f (x) \sim f (x) \)
--
--  \( \forall x : unit \circ g (x) \sim g (x) \)
module Data.Connection.Property where

import Data.Connection
import Data.Order
import Data.Order.Property
import Prelude hiding (Num (..), Ord (..), ceiling, floor)

-- | \( \forall x, y : f \dashv g \Rightarrow f (x) \leq y \Leftrightarrow x \leq g (y) \)
--
-- A Galois connection is an adjunction of preorders. This is a required property.
adjoint :: (Preorder a, Preorder b) => ConnK a b -> a -> b -> Bool
adjoint :: ConnK a b -> a -> b -> Bool
adjoint ConnK a b
t a
a b
b =
    ConnL a b -> a -> b -> Bool
forall a b. (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
adjointL ConnL a b
ConnK a b
t a
a b
b
        Bool -> Bool -> Bool
&& ConnR a b -> a -> b -> Bool
forall a b. (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
adjointR ConnR a b
ConnK a b
t a
a b
b
        Bool -> Bool -> Bool
&& ConnL b a -> b -> a -> Bool
forall a b. (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
adjointL (ConnR a b -> ConnL b a
forall a b. ConnR a b -> ConnL b a
swapL ConnR a b
ConnK a b
t) b
b a
a
        Bool -> Bool -> Bool
&& ConnR b a -> b -> a -> Bool
forall a b. (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
adjointR (ConnL a b -> ConnR b a
forall a b. ConnL a b -> ConnR b a
swapR ConnL a b
ConnK a b
t) b
b a
a

adjointL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
adjointL :: ConnL a b -> a -> b -> Bool
adjointL (ConnL a -> b
f b -> a
g) = Rel b Bool -> Rel a Bool -> (a -> b) -> (b -> a) -> a -> b -> Bool
forall r s.
Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool
adjunction Rel b Bool
forall a. Preorder a => a -> a -> Bool
(<~) Rel a Bool
forall a. Preorder a => a -> a -> Bool
(<~) a -> b
f b -> a
g

adjointR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
adjointR :: ConnR a b -> a -> b -> Bool
adjointR (ConnR b -> a
f a -> b
g) = Rel b Bool -> Rel a Bool -> (a -> b) -> (b -> a) -> a -> b -> Bool
forall r s.
Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool
adjunction Rel b Bool
forall a. Preorder a => a -> a -> Bool
(>~) Rel a Bool
forall a. Preorder a => a -> a -> Bool
(>~) a -> b
g b -> a
f

-- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \)
--
-- This is a required property.
closed :: (Preorder a, Preorder b) => ConnK a b -> a -> Bool
closed :: ConnK a b -> a -> Bool
closed ConnK a b
t a
a = ConnL a b -> a -> Bool
forall a b. (Preorder a, Preorder b) => ConnL a b -> a -> Bool
closedL ConnL a b
ConnK a b
t a
a Bool -> Bool -> Bool
&& ConnR a b -> a -> Bool
forall a b. (Preorder a, Preorder b) => ConnR a b -> a -> Bool
closedR ConnR a b
ConnK a b
t a
a

closedL :: (Preorder a, Preorder b) => ConnL a b -> a -> Bool
closedL :: ConnL a b -> a -> Bool
closedL (ConnL a -> b
f b -> a
g) = Rel a Bool -> (a -> b) -> (b -> a) -> a -> Bool
forall s b r. Rel s b -> (s -> r) -> (r -> s) -> s -> b
invertible Rel a Bool
forall a. Preorder a => a -> a -> Bool
(>~) a -> b
f b -> a
g

closedR :: (Preorder a, Preorder b) => ConnR a b -> a -> Bool
closedR :: ConnR a b -> a -> Bool
closedR (ConnR b -> a
f a -> b
g) = Rel a Bool -> (a -> b) -> (b -> a) -> a -> Bool
forall s b r. Rel s b -> (s -> r) -> (r -> s) -> s -> b
invertible Rel a Bool
forall a. Preorder a => a -> a -> Bool
(<~) a -> b
g b -> a
f

-- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \)
--
-- This is a required property.
kernel :: (Preorder a, Preorder b) => ConnK a b -> b -> Bool
kernel :: ConnK a b -> b -> Bool
kernel ConnK a b
t b
b = ConnL a b -> b -> Bool
forall a b. (Preorder a, Preorder b) => ConnL a b -> b -> Bool
kernelL ConnL a b
ConnK a b
t b
b Bool -> Bool -> Bool
&& ConnR a b -> b -> Bool
forall a b. (Preorder a, Preorder b) => ConnR a b -> b -> Bool
kernelR ConnR a b
ConnK a b
t b
b

kernelL :: (Preorder a, Preorder b) => ConnL a b -> b -> Bool
kernelL :: ConnL a b -> b -> Bool
kernelL (ConnL a -> b
f b -> a
g) = Rel b Bool -> (b -> a) -> (a -> b) -> b -> Bool
forall s b r. Rel s b -> (s -> r) -> (r -> s) -> s -> b
invertible Rel b Bool
forall a. Preorder a => a -> a -> Bool
(<~) b -> a
g a -> b
f

kernelR :: (Preorder a, Preorder b) => ConnR a b -> b -> Bool
kernelR :: ConnR a b -> b -> Bool
kernelR (ConnR b -> a
f a -> b
g) = Rel b Bool -> (b -> a) -> (a -> b) -> b -> Bool
forall s b r. Rel s b -> (s -> r) -> (r -> s) -> s -> b
invertible Rel b Bool
forall a. Preorder a => a -> a -> Bool
(>~) b -> a
f a -> b
g

-- | \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \)
--
-- This is a required property.
monotonic :: (Preorder a, Preorder b) => ConnK a b -> a -> a -> b -> b -> Bool
monotonic :: ConnK a b -> a -> a -> b -> b -> Bool
monotonic ConnK a b
t a
a1 a
a2 b
b1 b
b2 = ConnL a b -> a -> a -> b -> b -> Bool
forall a b.
(Preorder a, Preorder b) =>
ConnL a b -> a -> a -> b -> b -> Bool
monotonicL ConnL a b
ConnK a b
t a
a1 a
a2 b
b1 b
b2 Bool -> Bool -> Bool
&& ConnR a b -> a -> a -> b -> b -> Bool
forall a b.
(Preorder a, Preorder b) =>
ConnR a b -> a -> a -> b -> b -> Bool
monotonicR ConnR a b
ConnK a b
t a
a1 a
a2 b
b1 b
b2

monotonicR :: (Preorder a, Preorder b) => ConnR a b -> a -> a -> b -> b -> Bool
monotonicR :: ConnR a b -> a -> a -> b -> b -> Bool
monotonicR (ConnR b -> a
f a -> b
g) a
a1 a
a2 b
b1 b
b2 = Rel a Bool -> (b -> b -> Bool) -> (a -> b) -> Rel a Bool
forall r s. Rel r Bool -> Rel s Bool -> (r -> s) -> Rel r Bool
monotone Rel a Bool
forall a. Preorder a => a -> a -> Bool
(<~) b -> b -> Bool
forall a. Preorder a => a -> a -> Bool
(<~) a -> b
g a
a1 a
a2 Bool -> Bool -> Bool
&& (b -> b -> Bool) -> Rel a Bool -> (b -> a) -> b -> b -> Bool
forall r s. Rel r Bool -> Rel s Bool -> (r -> s) -> Rel r Bool
monotone b -> b -> Bool
forall a. Preorder a => a -> a -> Bool
(<~) Rel a Bool
forall a. Preorder a => a -> a -> Bool
(<~) b -> a
f b
b1 b
b2

monotonicL :: (Preorder a, Preorder b) => ConnL a b -> a -> a -> b -> b -> Bool
monotonicL :: ConnL a b -> a -> a -> b -> b -> Bool
monotonicL (ConnL a -> b
f b -> a
g) a
a1 a
a2 b
b1 b
b2 = Rel a Bool -> (b -> b -> Bool) -> (a -> b) -> Rel a Bool
forall r s. Rel r Bool -> Rel s Bool -> (r -> s) -> Rel r Bool
monotone Rel a Bool
forall a. Preorder a => a -> a -> Bool
(<~) b -> b -> Bool
forall a. Preorder a => a -> a -> Bool
(<~) a -> b
f a
a1 a
a2 Bool -> Bool -> Bool
&& (b -> b -> Bool) -> Rel a Bool -> (b -> a) -> b -> b -> Bool
forall r s. Rel r Bool -> Rel s Bool -> (r -> s) -> Rel r Bool
monotone b -> b -> Bool
forall a. Preorder a => a -> a -> Bool
(<~) Rel a Bool
forall a. Preorder a => a -> a -> Bool
(<~) b -> a
g b
b1 b
b2

-- | \( \forall x: f \dashv g \Rightarrow counit \circ f (x) \sim f (x) \wedge unit \circ g (x) \sim g (x) \)
--
-- See <https://ncatlab.org/nlab/show/idempotent+adjunction>
idempotent :: (Preorder a, Preorder b) => ConnK a b -> a -> b -> Bool
idempotent :: ConnK a b -> a -> b -> Bool
idempotent ConnK a b
t a
a b
b = ConnL a b -> a -> b -> Bool
forall a b. (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
idempotentL ConnL a b
ConnK a b
t a
a b
b Bool -> Bool -> Bool
&& ConnR a b -> a -> b -> Bool
forall a b. (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
idempotentR ConnR a b
ConnK a b
t a
a b
b

idempotentL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
idempotentL :: ConnL a b -> a -> b -> Bool
idempotentL c :: ConnL a b
c@(ConnL a -> b
f b -> a
g) a
a b
b = Rel a Bool -> (b -> a) -> (a -> a) -> b -> Bool
forall s b r. Rel s b -> (r -> s) -> (s -> s) -> r -> b
projective Rel a Bool
forall a. Preorder a => a -> a -> Bool
(~~) b -> a
g (ConnL a b -> a -> a
forall a b. ConnL a b -> a -> a
upper ConnL a b
c) b
b Bool -> Bool -> Bool
&& Rel b Bool -> (a -> b) -> (b -> b) -> a -> Bool
forall s b r. Rel s b -> (r -> s) -> (s -> s) -> r -> b
projective Rel b Bool
forall a. Preorder a => a -> a -> Bool
(~~) a -> b
f (ConnL a b -> b -> b
forall a b. ConnL a b -> b -> b
counit ConnL a b
c) a
a

idempotentR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
idempotentR :: ConnR a b -> a -> b -> Bool
idempotentR c :: ConnR a b
c@(ConnR b -> a
f a -> b
g) a
a b
b = Rel b Bool -> (a -> b) -> (b -> b) -> a -> Bool
forall s b r. Rel s b -> (r -> s) -> (s -> s) -> r -> b
projective Rel b Bool
forall a. Preorder a => a -> a -> Bool
(~~) a -> b
g (ConnR a b -> b -> b
forall a b. ConnR a b -> b -> b
unit ConnR a b
c) a
a Bool -> Bool -> Bool
&& Rel a Bool -> (b -> a) -> (a -> a) -> b -> Bool
forall s b r. Rel s b -> (r -> s) -> (s -> s) -> r -> b
projective Rel a Bool
forall a. Preorder a => a -> a -> Bool
(~~) b -> a
f (ConnR a b -> a -> a
forall a b. ConnR a b -> a -> a
lower ConnR a b
c) b
b

---------------------------------------------------------------------
-- Properties of general relations
---------------------------------------------------------------------

-- | \( \forall a, b: a \leq b \Rightarrow f(a) \leq f(b) \)
monotone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool
monotone :: Rel r Bool -> Rel s Bool -> (r -> s) -> Rel r Bool
monotone Rel r Bool
(#) Rel s Bool
(%) r -> s
f r
a r
b = r
a Rel r Bool
# r
b Bool -> Bool -> Bool
==> r -> s
f r
a Rel s Bool
% r -> s
f r
b

-- | \( \forall a, b: a \leq b \Rightarrow f(b) \leq f(a) \)
antitone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool
antitone :: Rel r Bool -> Rel s Bool -> (r -> s) -> Rel r Bool
antitone Rel r Bool
(#) Rel s Bool
(%) r -> s
f r
a r
b = r
a Rel r Bool
# r
b Bool -> Bool -> Bool
==> r -> s
f r
b Rel s Bool
% r -> s
f r
a

-- | \( \forall a: f a \leq b \Leftrightarrow a \leq g b \)
--
-- For example, a monotone Galois connection is defined by @adjunction (<~) (<~)@,
-- and an antitone Galois connection is defined by @adjunction (>~) (<~)@.
adjunction :: Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool
adjunction :: Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool
adjunction Rel r Bool
(#) Rel s Bool
(%) s -> r
f r -> s
g s
a r
b = s -> r
f s
a Rel r Bool
# r
b Bool -> Bool -> Bool
<=> s
a Rel s Bool
% r -> s
g r
b

-- | \( \forall a: f (g a) \sim a \)
invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b
invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b
invertible Rel s b
(#) s -> r
f r -> s
g s
a = r -> s
g (s -> r
f s
a) Rel s b
# s
a

-- | \( \forall a: g \circ f (a) \sim f (a) \)
--
-- > idempotent (#) f = projective (#) f f
projective :: Rel s b -> (r -> s) -> (s -> s) -> r -> b
projective :: Rel s b -> (r -> s) -> (s -> s) -> r -> b
projective Rel s b
(#) r -> s
f s -> s
g r
r = s -> s
g (r -> s
f r
r) Rel s b
# r -> s
f r
r