module Proarrow.Category.Instance.Sub where

import Proarrow.Core (CAT, OB, UN, Is, CategoryOf (..), Promonad (..), Profunctor (..), dimapDefault)
import Proarrow.Category.Monoidal (Monoidal (..), SymMonoidal (..), MonoidalProfunctor (..))


type data SUBCAT (ob :: OB k) = SUB k
type instance UN SUB (SUB k) = k

type Sub :: CAT (SUBCAT ob)
data Sub a b where
  Sub :: (ob a, ob b) => a ~> b -> Sub (SUB a :: SUBCAT ob) (SUB b)

instance Profunctor ((~>) :: CAT k) => Profunctor (Sub :: CAT (SUBCAT (ob :: OB k))) where
  dimap :: forall (c :: SUBCAT ob) (a :: SUBCAT ob) (b :: SUBCAT ob)
       (d :: SUBCAT ob).
(c ~> a) -> (b ~> d) -> Sub a b -> Sub c d
dimap = (c ~> a) -> (b ~> d) -> Sub a b -> Sub c d
Sub c a -> Sub b d -> Sub a b -> Sub c d
forall {k} (p :: PRO 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 :: SUBCAT ob) (b :: SUBCAT ob) r.
((Ob a, Ob b) => r) -> Sub a b -> r
\\ Sub a ~> b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> b
p

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

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 (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)
  Sub a ~> b
f par :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (c :: SUBCAT ob)
       (d :: SUBCAT ob).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Sub a ~> b
g = ((a ** a) ~> (b ** b)) -> Sub (SUB (a ** a)) (SUB (b ** b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
(ob a, ob b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (a ~> b
f (a ~> b) -> (a ~> b) -> (a ** a) ~> (b ** b)
forall (a :: k) (b :: k) (c :: k) (d :: k).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` a ~> b
g)
  leftUnitor :: forall (a :: SUBCAT ob). Obj a -> (Unit ** a) ~> a
leftUnitor (Sub a ~> b
a) = ((Unit ** b) ~> b) -> Sub (SUB (Unit ** b)) (SUB b)
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
(ob a, ob b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> (Unit ** b) ~> b
forall (a :: k). Obj a -> (Unit ** a) ~> a
forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a
leftUnitor a ~> b
Obj b
a)
  leftUnitorInv :: forall (a :: SUBCAT ob). Obj a -> a ~> (Unit ** a)
leftUnitorInv (Sub a ~> b
a) = (b ~> (Unit ** b)) -> Sub (SUB b) (SUB (Unit ** b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
(ob a, ob b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> b ~> (Unit ** b)
forall (a :: k). Obj a -> a ~> (Unit ** a)
forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a)
leftUnitorInv a ~> b
Obj b
a)
  rightUnitor :: forall (a :: SUBCAT ob). Obj a -> (a ** Unit) ~> a
rightUnitor (Sub a ~> b
a) = ((b ** Unit) ~> b) -> Sub (SUB (b ** Unit)) (SUB b)
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
(ob a, ob b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> (b ** Unit) ~> b
forall (a :: k). Obj a -> (a ** Unit) ~> a
forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a
rightUnitor a ~> b
Obj b
a)
  rightUnitorInv :: forall (a :: SUBCAT ob). Obj a -> a ~> (a ** Unit)
rightUnitorInv (Sub a ~> b
a) = (b ~> (b ** Unit)) -> Sub (SUB b) (SUB (b ** Unit))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
(ob a, ob b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> b ~> (b ** Unit)
forall (a :: k). Obj a -> a ~> (a ** Unit)
forall k (a :: k). Monoidal k => Obj a -> a ~> (a ** Unit)
rightUnitorInv a ~> b
Obj b
a)
  associator :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (c :: SUBCAT ob).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator (Sub a ~> b
a) (Sub a ~> b
b) (Sub a ~> b
c) = (((b ** b) ** b) ~> (b ** (b ** b)))
-> Sub (SUB ((b ** b) ** b)) (SUB (b ** (b ** b)))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
(ob a, ob b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> Obj b -> Obj b -> ((b ** b) ** b) ~> (b ** (b ** b))
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator a ~> b
Obj b
a a ~> b
Obj b
b a ~> b
Obj b
c)
  associatorInv :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (c :: SUBCAT ob).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv (Sub a ~> b
a) (Sub a ~> b
b) (Sub a ~> b
c) = ((b ** (b ** b)) ~> ((b ** b) ** b))
-> Sub (SUB (b ** (b ** b))) (SUB ((b ** b) ** b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
(ob a, ob b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> Obj b -> Obj b -> (b ** (b ** b)) ~> ((b ** b) ** b)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall k (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv a ~> b
Obj b
a a ~> b
Obj b
b a ~> b
Obj 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) (b :: SUBCAT ob).
Obj a -> Obj b -> (a ** b) ~> (b ** a)
swap' (Sub a ~> b
a) (Sub a ~> b
b) = ((b ** b) ~> (b ** b)) -> Sub (SUB (b ** b)) (SUB (b ** b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k).
(ob a, ob b) =>
(a ~> b) -> Sub (SUB a) (SUB b)
Sub (Obj b -> Obj b -> (b ** b) ~> (b ** b)
forall (a :: k) (b :: k). Obj a -> Obj b -> (a ** b) ~> (b ** a)
forall k (a :: k) (b :: k).
SymMonoidal k =>
Obj a -> Obj b -> (a ** b) ~> (b ** a)
swap' a ~> b
Obj b
a a ~> b
Obj b
b)

instance (Monoidal k, ob Unit, forall a b. (ob a, ob b) => IsObMult ob a b) => MonoidalProfunctor (Sub :: CAT (SUBCAT (ob :: OB k))) where
  lift0 :: Sub Unit Unit
lift0 = Sub Unit Unit
Sub (SUB Unit) (SUB Unit)
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: SUBCAT ob). Ob a => Sub a a
id
  lift2 :: forall (x1 :: SUBCAT ob) (x2 :: SUBCAT ob) (y1 :: SUBCAT ob)
       (y2 :: SUBCAT ob).
Sub x1 x2 -> Sub y1 y2 -> Sub (x1 ** y1) (x2 ** y2)
lift2 = (x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
Sub x1 x2 -> Sub y1 y2 -> Sub (x1 ** y1) (x2 ** y2)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall (a :: SUBCAT ob) (b :: SUBCAT ob) (c :: SUBCAT ob)
       (d :: SUBCAT ob).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
par