module Proarrow.Category.Instance.Sub where

import Data.Kind (Constraint, Type)

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, OB, Profunctor (..), Promonad (..), UN, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Profunctor.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 (ob (a ** b)) => IsObMult (ob :: OB k) a b
instance (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)

data family Forget :: forall (ob :: OB k) -> SUBCAT ob +-> k
instance (CategoryOf k) => FunctorForRep (Forget (ob :: OB k)) where
  type Forget ob @ (SUB a) = a
  fmap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(a ~> b) -> (Forget ob @ a) ~> (Forget ob @ b)
fmap (Sub a ~> b
f) = a ~> b
(Forget ob @ a) ~> (Forget ob @ b)
f

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)