module Proarrow.Category.Instance.Sub where

import Data.Kind (Constraint, Type)

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, OB, Profunctor (..), Promonad (..), UN, type (+->))
import Proarrow.Profunctor.Representable (Representable (..))

type SUBCAT :: forall {k}. OB k -> Type
type data SUBCAT (ob :: OB k) = SUB k
type instance UN SUB (SUB k) = k

type Sub :: CAT k -> CAT (SUBCAT (ob :: OB k))
data Sub p a b where
  Sub :: (ob a, ob b) => {forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
Sub p (SUB a) (SUB b) -> p a b
unSub :: p a b} -> Sub p (SUB a :: SUBCAT ob) (SUB b)

instance (Profunctor p) => Profunctor (Sub p) where
  dimap :: forall (c :: SUBCAT ob) (a :: SUBCAT ob) (b :: SUBCAT ob)
       (d :: SUBCAT ob).
(c ~> a) -> (b ~> d) -> Sub p a b -> Sub p c d
dimap (Sub a ~> b
l) (Sub a ~> b
r) (Sub p a b
p) = p a b -> Sub p (SUB a) (SUB b)
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub ((a ~> a) -> (b ~> b) -> p a b -> p a b
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> b
a ~> a
l a ~> b
b ~> b
r p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) r.
((Ob a, Ob b) => r) -> Sub p a b -> r
\\ Sub p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance (Promonad p) => Promonad (Sub p) where
  id :: forall (a :: SUBCAT ob). Ob a => Sub p a a
id = p (UN SUB a) (UN SUB a) -> Sub p (SUB (UN SUB a)) (SUB (UN SUB a))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub p (UN SUB a) (UN SUB a)
forall (a :: k). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Sub p a b
f . :: forall (b :: SUBCAT ob) (c :: SUBCAT ob) (a :: SUBCAT ob).
Sub p b c -> Sub p a b -> Sub p a c
. Sub p a b
g = p a b -> Sub p (SUB a) (SUB b)
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (p a b
f p a b -> p a a -> p a b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p 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
. p a a
p a b
g)

-- | The subcategory with objects with instances of the given constraint `ob`.
instance (CategoryOf k) => CategoryOf (SUBCAT (ob :: OB k)) where
  type (~>) = Sub (~>)
  type Ob (a :: SUBCAT ob) = (Is SUB a, Ob (UN SUB a), ob (UN SUB a))

type On :: (k -> Constraint) -> forall (ob :: OB k) -> SUBCAT ob -> Constraint
class (c (UN SUB a)) => (c `On` ob) a
instance (c (UN SUB a)) => (c `On` ob) a

class (CategoryOf k, ob (a ** b)) => IsObMult (ob :: OB k) a b
instance (CategoryOf k, ob (a ** b)) => IsObMult (ob :: OB k) a b

instance
  (MonoidalProfunctor p, ob Unit, forall a b. (ob a, ob b) => IsObMult ob a b)
  => MonoidalProfunctor (Sub p :: CAT (SUBCAT (ob :: OB k)))
  where
  par0 :: Sub p Unit Unit
par0 = p Unit Unit -> Sub p (SUB Unit) (SUB Unit)
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  Sub p a b
f par :: forall (x1 :: SUBCAT ob) (x2 :: SUBCAT ob) (y1 :: SUBCAT ob)
       (y2 :: SUBCAT ob).
Sub p x1 x2 -> Sub p y1 y2 -> Sub p (x1 ** y1) (x2 ** y2)
`par` Sub p a b
g = p (a ** a) (b ** b) -> Sub p (SUB (a ** a)) (SUB (b ** b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (p a b
f p a b -> p a b -> p (a ** a) (b ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` p a b
g)

instance (Monoidal k, ob Unit, forall a b. (ob a, ob b) => IsObMult ob a b) => Monoidal (SUBCAT (ob :: OB k)) where
  type Unit = SUB Unit
  type a ** b = SUB (UN SUB a ** UN SUB b)
  leftUnitor :: forall (a :: SUBCAT ob). Ob a => (Unit ** a) ~> a
leftUnitor = ((Unit ** UN SUB a) ~> UN SUB a)
-> Sub (~>) (SUB (Unit ** UN SUB a)) (SUB (UN SUB a))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (Unit ** UN SUB a) ~> UN SUB a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  leftUnitorInv :: forall (a :: SUBCAT ob). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN SUB a ~> (Unit ** UN SUB a))
-> Sub (~>) (SUB (UN SUB a)) (SUB (Unit ** UN SUB a))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub UN SUB a ~> (Unit ** UN SUB a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  rightUnitor :: forall (a :: SUBCAT ob). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN SUB a ** Unit) ~> UN SUB a)
-> Sub (~>) (SUB (UN SUB a ** Unit)) (SUB (UN SUB a))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (UN SUB a ** Unit) ~> UN SUB a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
  rightUnitorInv :: forall (a :: SUBCAT ob). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN SUB a ~> (UN SUB a ** Unit))
-> Sub (~>) (SUB (UN SUB a)) (SUB (UN SUB a ** Unit))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub UN SUB a ~> (UN SUB a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
  associator :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (c :: SUBCAT ob).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(SUB a) @(SUB b) @(SUB c) = (((UN SUB a ** UN SUB b) ** UN SUB c)
 ~> (UN SUB a ** (UN SUB b ** UN SUB c)))
-> Sub
     (~>)
     (SUB ((UN SUB a ** UN SUB b) ** UN SUB c))
     (SUB (UN SUB a ** (UN SUB b ** UN SUB c)))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @a @b @c)
  associatorInv :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (c :: SUBCAT ob).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(SUB a) @(SUB b) @(SUB c) = ((UN SUB a ** (UN SUB b ** UN SUB c))
 ~> ((UN SUB a ** UN SUB b) ** UN SUB c))
-> Sub
     (~>)
     (SUB (UN SUB a ** (UN SUB b ** UN SUB c)))
     (SUB ((UN SUB a ** UN SUB b) ** UN SUB c))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @a @b @c)

instance (SymMonoidal k, ob Unit, forall a b. (ob a, ob b) => IsObMult ob a b) => SymMonoidal (SUBCAT (ob :: OB k)) where
  swap' :: forall (a :: SUBCAT ob) (a' :: SUBCAT ob) (b :: SUBCAT ob)
       (b' :: SUBCAT ob).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' (Sub a ~> b
a) (Sub a ~> b
b) = ((a ** a) ~> (b ** b)) -> Sub (~>) (SUB (a ** a)) (SUB (b ** b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub ((a ~> b) -> (a ~> b) -> (a ** a) ~> (b ** b)
forall (a :: k) (a' :: k) (b :: k) (b' :: k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' a ~> b
a a ~> b
b)

instance (Representable p, forall a. (ob a) => ob (p % a)) => Representable (Sub p :: CAT (SUBCAT (ob :: OB k))) where
  type Sub p % a = SUB (p % UN SUB a)
  index :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
Sub p a b -> a ~> (Sub p % b)
index (Sub p a b
p) = (a ~> (p % b)) -> Sub (~>) (SUB a) (SUB (p % b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (p a b -> a ~> (p % b)
forall (a :: k) (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 a b
p)
  tabulate :: forall (b :: SUBCAT ob) (a :: SUBCAT ob).
Ob b =>
(a ~> (Sub p % b)) -> Sub p a b
tabulate (Sub a ~> b
f) = p a (UN SUB b) -> Sub p (SUB a) (SUB (UN SUB b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub ((a ~> (p % UN SUB b)) -> p a (UN SUB b)
forall (b :: k) (a :: k). 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 a ~> b
a ~> (p % UN SUB b)
f)
  repMap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(a ~> b) -> (Sub p % a) ~> (Sub p % b)
repMap (Sub a ~> b
f) = ((p % a) ~> (p % b)) -> Sub (~>) (SUB (p % a)) (SUB (p % b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a ~> b
f)

instance (Strong w p, Monoidal (SUBCAT (ob :: OB m))) => Strong (Sub w :: CAT (SUBCAT (ob :: OB m))) (p :: Type +-> Type) where
  Sub w a b
f act :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) x y.
Sub w a b -> p x y -> p (Act a x) (Act b y)
`act` p x y
g = w a b
f w a b -> p x y -> p (Act a x) (Act b y)
forall (a :: m) (b :: m) x y.
w a b -> p x y -> p (Act a x) (Act b y)
forall {m} {m'} {c} {d} (w :: m +-> m') (p :: c +-> d) (a :: m')
       (b :: m) (x :: d) (y :: c).
Strong w p =>
w a b -> p x y -> p (Act a x) (Act b y)
`act` p x y
g
instance (MonoidalAction m Type, Monoidal (SUBCAT (ob :: OB m))) => MonoidalAction (SUBCAT (ob :: OB m)) Type where
  type Act (p :: SUBCAT ob) (x :: Type) = Act (UN SUB p) x
  unitor :: forall x. Ob x => Act Unit x ~> x
unitor = forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m
  unitorInv :: forall x. Ob x => x ~> Act Unit x
unitorInv = forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m
  multiplicator :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) x.
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @(SUB p) @(SUB q) @x = forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @_ @_ @p @q @x
  multiplicatorInv :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) x.
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @(SUB p) @(SUB q) @x = forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @_ @_ @p @q @x