module Proarrow.Preorder.ThinCategory where

import Data.Kind (Constraint)
import Prelude (type (~))

import Proarrow.Core (CategoryOf(..), UN, Is, obj, Promonad (..), Profunctor (..), CAT, type (+->))
import Proarrow.Preorder (CProfunctor (..), POS, cdimapDefault, CPromonad (..), PreorderOf(..), type (:-) (..), Dict (..))

type ThinProfunctor :: forall {j} {k}. j +-> k -> Constraint
class Profunctor p => ThinProfunctor (p :: j +-> k) where
  type HasArrow (p :: j +-> k) (a :: k) (b :: j) :: Constraint
  type HasArrow p a b = ()
  arr :: (Ob a, Ob b, HasArrow p a b) => p a b
  withArr :: p a b -> (HasArrow p a b => r) -> r

class (ThinProfunctor ((~>) :: CAT k)) => Thin k
instance (ThinProfunctor ((~>) :: CAT k)) => Thin k

class HasArrow p a b => HasArrow' p a b
instance HasArrow p a b => HasArrow' p a b

class (ThinProfunctor p) => Codiscrete p where
  anyArr :: (Ob a, Ob b) => p a b
  default anyArr :: (Ob a, Ob b, forall c d. (Ob c, Ob d) => HasArrow' p c d) => p a b
  anyArr = 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

class (ThinProfunctor p) => Discrete p where
  withEq :: p a b -> (a ~ b => r) -> r
  default withEq :: (forall c d. HasArrow' p c d => c ~ d) => p a b -> (a ~ b => r) -> r
  withEq = p a b -> ((a ~ b) => r) -> r
p a b -> (HasArrow p a b => r) -> r
forall (a :: k) (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

newtype THIN k = T k
type instance UN T (T a) = a

class (Thin k, HasArrow (~>) (UN T a) (UN T b), COb a, COb b) => ThinCategory (a :: THIN k) b
instance (Thin k, HasArrow (~>) (UN T a) (UN T b), COb a, COb b) => ThinCategory (a :: THIN k) b

instance Thin k => CProfunctor (ThinCategory :: POS (THIN k)) where
  cdimap :: forall (c :: THIN k) (a :: THIN k) (b :: THIN k) (d :: THIN k).
(c <= a, b <= d, ThinCategory a b) :- ThinCategory c d
cdimap = (c <= a, b <= d, ThinCategory a b) :- ThinCategory c d
(ThinCategory c a, ThinCategory b d, ThinCategory a b)
:- ThinCategory c d
forall {k} (p :: k -> k -> Constraint) (a :: k) (b :: k) (c :: k)
       (d :: k).
CPromonad p =>
(p c a, p b d, p a b) :- p c d
cdimapDefault
  obs :: forall (a :: THIN k) (b :: THIN k).
ThinCategory a b :- (COb a, COb b)
obs = (ThinCategory a b =>
 Dict
   ((a ~ 'T (UN 'T a), Ob (UN 'T a)),
    (b ~ 'T (UN 'T b), Ob (UN 'T b))))
-> ThinCategory a b
   :- ((a ~ 'T (UN 'T a), Ob (UN 'T a)),
       (b ~ 'T (UN 'T b), Ob (UN 'T b)))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict
  ((a ~ 'T (UN 'T a), Ob (UN 'T a)),
   (b ~ 'T (UN 'T b), Ob (UN 'T b)))
ThinCategory a b =>
Dict
  ((a ~ 'T (UN 'T a), Ob (UN 'T a)),
   (b ~ 'T (UN 'T b), Ob (UN 'T b)))
forall (a :: Constraint). a => Dict a
Dict
instance Thin k => CPromonad (ThinCategory :: POS (THIN k)) where
  cid :: forall (a :: THIN k).
COb a =>
(() :: Constraint) :- ThinCategory a a
cid @(T a) = ((() :: Constraint) => Dict (ThinCategory a a))
-> (() :: Constraint) :- ThinCategory a a
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((UN 'T a ~> UN 'T a)
-> (HasArrow (~>) (UN 'T a) (UN 'T a) => Dict (ThinCategory a a))
-> Dict (ThinCategory a a)
forall (a :: k) (b :: k) r.
(a ~> b) -> (HasArrow (~>) 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 (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) Dict (ThinCategory a a)
HasArrow (~>) (UN 'T a) (UN 'T a) => Dict (ThinCategory a a)
forall (a :: Constraint). a => Dict a
Dict)
  ccomp :: forall (a :: THIN k) (b :: THIN k) (c :: THIN k).
(ThinCategory b c, ThinCategory a b) :- ThinCategory a c
ccomp @a @b @c = ((ThinCategory b c, ThinCategory a b) => Dict (ThinCategory a c))
-> (ThinCategory b c, ThinCategory a b) :- ThinCategory a c
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((UN 'T a ~> UN 'T c)
-> (HasArrow (~>) (UN 'T a) (UN 'T c) => Dict (ThinCategory a c))
-> Dict (ThinCategory a c)
forall (a :: k) (b :: k) r.
(a ~> b) -> (HasArrow (~>) 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 (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 :: k +-> k) (a :: k) (b :: k).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @(~>) @(UN T b) @(UN T c) (UN 'T b ~> UN 'T c) -> (UN 'T a ~> UN 'T b) -> UN 'T a ~> UN 'T c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. 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 :: k +-> k) (a :: k) (b :: k).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr @(~>) @(UN T a) @(UN T b)) Dict (ThinCategory a c)
HasArrow (~>) (UN 'T a) (UN 'T c) => Dict (ThinCategory a c)
forall (a :: Constraint). a => Dict a
Dict)

instance Thin k => PreorderOf (THIN k) where
  type (<=) = ThinCategory
  type COb a = (Is T a, Ob (UN T a))