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)
import Proarrow.Monoid (CopyDiscard (..))
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 :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
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 :: j +-> k) (a :: k) (b :: j) 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 :: 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 :: 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, SubMonoidal ob) => 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)

class (Monoidal k, ob Unit, forall a b. (ob a, ob b) => IsObMult ob a b) => SubMonoidal (ob :: OB k)
instance (Monoidal k, ob Unit, forall a b. (ob a, ob b) => IsObMult ob a b) => SubMonoidal (ob :: OB k)

instance (SubMonoidal ob) => Monoidal (SUBCAT (ob :: OB k)) where
  type Unit = SUB Unit
  type a ** b = SUB (UN SUB a ** UN SUB b)
  withOb2 :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(SUB a) @(SUB b) Ob (a ** b) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @b r
Ob (UN SUB a ** UN SUB b) => r
Ob (a ** b) => r
r
  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, SubMonoidal ob) => SymMonoidal (SUBCAT (ob :: OB k)) where
  swap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(SUB a) @(SUB b) = ((UN SUB a ** UN SUB b) ~> (UN SUB b ** UN SUB a))
-> Sub
     (~>) (SUB (UN SUB a ** UN SUB b)) (SUB (UN SUB b ** 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 (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @b)

instance (SubMonoidal ob, CopyDiscard k) => CopyDiscard (SUBCAT (ob :: OB k)) where
  copy :: forall (a :: SUBCAT ob). Ob a => a ~> (a ** a)
copy = (UN SUB a ~> (UN SUB a ** UN SUB a))
-> Sub (~>) (SUB (UN SUB a)) (SUB (UN SUB a ** 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 ~> (UN SUB a ** UN SUB a)
forall (a :: k). Ob a => a ~> (a ** a)
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy
  discard :: forall (a :: SUBCAT ob). Ob a => a ~> Unit
discard = (UN SUB a ~> Unit) -> Sub (~>) (SUB (UN SUB a)) (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 UN SUB a ~> Unit
forall (a :: k). Ob a => a ~> Unit
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard

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 (MonoidalAction m Type, Monoidal (SUBCAT (ob :: OB m))) => Strong (SUBCAT (ob :: OB m)) (->) where
  Sub a ~> b
f act :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) x y.
(a ~> b) -> (x -> y) -> Act a x -> Act b y
`act` x -> y
g = a ~> b
f (a ~> b) -> (x -> y) -> Act a x -> Act b y
forall (a :: m) (b :: m) x y.
(a ~> b) -> (x -> y) -> Act a x -> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` 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
  withObAct :: forall (a :: SUBCAT ob) x r.
(Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct Ob (Act a x) => r
r = r
Ob (Act a x) => r
r
  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