module Proarrow.Category.Instance.PreorderAsCategory where

import Data.Kind (Constraint)

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor, Promonad (..), UN, dimapDefault)
import Proarrow.Core qualified as Core
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.BinaryProduct qualified as P
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Preorder (CProfunctor (..), CPromonad (..), PreorderOf (..), (\\))
import Proarrow.Preorder.Constraint ()
import Proarrow.Preorder.ThinCategory (ThinProfunctor (..))
import Proarrow.Category.Dagger (DaggerProfunctor (..))
import Proarrow.Preorder.Discrete (DISCRETE)

newtype POCATK k = PC k
type instance UN PC (PC k) = k

data PoAsCat a b where
  PoAsCat :: (a <= b) => PoAsCat (PC a) (PC b)

instance (PreorderOf k) => Profunctor (PoAsCat :: CAT (POCATK k)) where
  dimap :: forall (c :: POCATK k) (a :: POCATK k) (b :: POCATK k)
       (d :: POCATK k).
(c ~> a) -> (b ~> d) -> PoAsCat a b -> PoAsCat c d
dimap = (c ~> a) -> (b ~> d) -> PoAsCat a b -> PoAsCat c d
PoAsCat c a -> PoAsCat b d -> PoAsCat a b -> PoAsCat c d
forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: POCATK k) (b :: POCATK k) r.
((Ob a, Ob b) => r) -> PoAsCat a b -> r
\\ PoAsCat @a @b = r
(COb a, COb b) => r
(Ob a, Ob b) => r
r ((COb a, COb b) => r) -> ((a <= b) :- (COb a, COb b)) -> r
forall (a :: Constraint) (c :: Constraint) r.
a =>
(c => r) -> (a :- c) -> r
\\ forall {k} (p :: k -> k -> Constraint) (a :: k) (b :: k).
CProfunctor p =>
p a b :- (COb a, COb b)
forall (p :: k -> k -> Constraint) (a :: k) (b :: k).
CProfunctor p =>
p a b :- (COb a, COb b)
obs @((<=) @k) @a @b
instance (PreorderOf k) => Promonad (PoAsCat :: CAT (POCATK k)) where
  id :: forall (a :: POCATK k). Ob a => PoAsCat a a
id @a = PoAsCat a a
PoAsCat ('PC (UN 'PC a)) ('PC (UN 'PC a))
(UN 'PC a <= UN 'PC a) => PoAsCat a a
forall {k} (a :: k) (b :: k). (a <= b) => PoAsCat ('PC a) ('PC b)
PoAsCat ((UN 'PC a <= UN 'PC a) => PoAsCat a a)
-> ((() :: Constraint) :- (UN 'PC a <= UN 'PC a)) -> PoAsCat a a
forall (a :: Constraint) (c :: Constraint) r.
a =>
(c => r) -> (a :- c) -> r
\\ forall {k} (p :: k -> k -> Constraint) (a :: k).
(CPromonad p, COb a) =>
(() :: Constraint) :- p a a
forall (p :: k -> k -> Constraint) (a :: k).
(CPromonad p, COb a) =>
(() :: Constraint) :- p a a
cid @((<=) @k) @(UN PC a)
  . :: forall (b :: POCATK k) (c :: POCATK k) (a :: POCATK k).
PoAsCat b c -> PoAsCat a b -> PoAsCat a c
(.) @b @c @a PoAsCat b c
PoAsCat PoAsCat a b
PoAsCat = PoAsCat a c
PoAsCat ('PC a) ('PC b)
(a <= b) => PoAsCat a c
forall {k} (a :: k) (b :: k). (a <= b) => PoAsCat ('PC a) ('PC b)
PoAsCat ((a <= b) => PoAsCat a c)
-> ((a <= b, a <= a) :- (a <= b)) -> PoAsCat a c
forall (a :: Constraint) (c :: Constraint) r.
a =>
(c => r) -> (a :- c) -> r
\\ forall {k} (p :: k -> k -> Constraint) (a :: k) (b :: k) (c :: k).
CPromonad p =>
(p b c, p a b) :- p a c
forall (p :: k -> k -> Constraint) (a :: k) (b :: k) (c :: k).
CPromonad p =>
(p b c, p a b) :- p a c
ccomp @((<=) @k) @(UN PC a) @(UN PC b) @(UN PC c)
-- | The preorder as a category.
instance (PreorderOf k) => CategoryOf (POCATK k) where
  type (~>) = PoAsCat
  type Ob a = (Is PC a, COb (UN PC a))

instance (PreorderOf k) => ThinProfunctor (PoAsCat :: CAT (POCATK k)) where
  type HasArrow PoAsCat (PC a) (PC b) = a <= b
  arr :: forall (a :: POCATK k) (b :: POCATK k).
(Ob a, Ob b, HasArrow PoAsCat a b) =>
PoAsCat a b
arr = PoAsCat a b
PoAsCat ('PC (UN 'PC a)) ('PC (UN 'PC b))
forall {k} (a :: k) (b :: k). (a <= b) => PoAsCat ('PC a) ('PC b)
PoAsCat
  withArr :: forall (a :: POCATK k) (b :: POCATK k) r.
PoAsCat a b -> (HasArrow PoAsCat a b => r) -> r
withArr PoAsCat a b
PoAsCat HasArrow PoAsCat a b => r
r = r
HasArrow PoAsCat a b => r
r

instance HasTerminalObject (POCATK Constraint) where
  type TerminalObject = PC (() :: Constraint)
  terminate :: forall (a :: POCATK Constraint). Ob a => a ~> TerminalObject
terminate = a ~> TerminalObject
PoAsCat ('PC (UN 'PC a)) ('PC (() :: Constraint))
forall {k} (a :: k) (b :: k). (a <= b) => PoAsCat ('PC a) ('PC b)
PoAsCat

instance HasBinaryProducts (POCATK Constraint) where
  type l && r = PC ((UN PC l, UN PC r) :: Constraint)
  withObProd :: forall (a :: POCATK Constraint) (b :: POCATK Constraint) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: POCATK Constraint) (b :: POCATK Constraint).
(Ob a, Ob b) =>
(a && b) ~> a
fst = (a && b) ~> a
PoAsCat ('PC (UN 'PC a, UN 'PC b)) ('PC (UN 'PC a))
forall {k} (a :: k) (b :: k). (a <= b) => PoAsCat ('PC a) ('PC b)
PoAsCat
  snd :: forall (a :: POCATK Constraint) (b :: POCATK Constraint).
(Ob a, Ob b) =>
(a && b) ~> b
snd = (a && b) ~> b
PoAsCat ('PC (UN 'PC a, UN 'PC b)) ('PC (UN 'PC b))
forall {k} (a :: k) (b :: k). (a <= b) => PoAsCat ('PC a) ('PC b)
PoAsCat
  a ~> x
PoAsCat a x
PoAsCat &&& :: forall (a :: POCATK Constraint) (x :: POCATK Constraint)
       (y :: POCATK Constraint).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
PoAsCat ('PC a) y
PoAsCat = a ~> (x && y)
PoAsCat ('PC a) ('PC (b, b))
forall {k} (a :: k) (b :: k). (a <= b) => PoAsCat ('PC a) ('PC b)
PoAsCat

instance MonoidalProfunctor (PoAsCat :: CAT (POCATK Constraint)) where
  par0 :: PoAsCat Unit Unit
par0 = PoAsCat Unit Unit
PoAsCat ('PC (() :: Constraint)) ('PC (() :: Constraint))
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: POCATK Constraint). Ob a => PoAsCat a a
id
  PoAsCat x1 x2
f par :: forall (x1 :: POCATK Constraint) (x2 :: POCATK Constraint)
       (y1 :: POCATK Constraint) (y2 :: POCATK Constraint).
PoAsCat x1 x2 -> PoAsCat y1 y2 -> PoAsCat (x1 ** y1) (x2 ** y2)
`par` PoAsCat y1 y2
g = x1 ~> x2
PoAsCat x1 x2
f (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall (a :: POCATK Constraint) (b :: POCATK Constraint)
       (x :: POCATK Constraint) (y :: POCATK Constraint).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** y1 ~> y2
PoAsCat y1 y2
g

-- | Products as monoidal structure.
instance Monoidal (POCATK Constraint) where
  type Unit = TerminalObject
  type a ** b = a && b
  withOb2 :: forall (a :: POCATK Constraint) (b :: POCATK Constraint) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: POCATK Constraint). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && 'PC (UN 'PC a)) ~> 'PC (UN 'PC a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
P.leftUnitorProd
  leftUnitorInv :: forall (a :: POCATK Constraint). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
'PC (UN 'PC a) ~> (TerminalObject && 'PC (UN 'PC a))
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
P.leftUnitorProdInv
  rightUnitor :: forall (a :: POCATK Constraint). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
('PC (UN 'PC a) && TerminalObject) ~> 'PC (UN 'PC a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
P.rightUnitorProd
  rightUnitorInv :: forall (a :: POCATK Constraint). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
'PC (UN 'PC a) ~> ('PC (UN 'PC a) && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
P.rightUnitorProdInv
  associator :: forall (a :: POCATK Constraint) (b :: POCATK Constraint)
       (c :: POCATK Constraint).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = ((a ** b) ** c) ~> (a ** (b ** c))
(('PC (UN 'PC a) && 'PC (UN 'PC b)) && 'PC (UN 'PC c))
~> ('PC (UN 'PC a) && ('PC (UN 'PC b) && 'PC (UN 'PC c)))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
P.associatorProd
  associatorInv :: forall (a :: POCATK Constraint) (b :: POCATK Constraint)
       (c :: POCATK Constraint).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ** (b ** c)) ~> ((a ** b) ** c)
('PC (UN 'PC a) && ('PC (UN 'PC b) && 'PC (UN 'PC c)))
~> (('PC (UN 'PC a) && 'PC (UN 'PC b)) && 'PC (UN 'PC c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
P.associatorProdInv

instance DaggerProfunctor (PoAsCat :: CAT (POCATK (DISCRETE k))) where
  dagger :: forall (a :: POCATK (DISCRETE k)) (b :: POCATK (DISCRETE k)).
PoAsCat a b -> PoAsCat b a
dagger PoAsCat a b
PoAsCat = PoAsCat b a
PoAsCat ('PC b) ('PC b)
forall {k} (a :: k) (b :: k). (a <= b) => PoAsCat ('PC a) ('PC b)
PoAsCat