{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Object.Copower where

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

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Core (CategoryOf (..), Ob, Profunctor (..), Promonad (..), type (+->))
import Proarrow.Object.Power (Powered (..))
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Enriched (Enriched, HomObj)
import Proarrow.Object.Exponential (Closed)

-- | Categories copowered over Hask.
class (Enriched v k, Closed v) => Copowered v k where
  type (n :: v) *. (a :: k) :: k
  withObCopower :: (Ob (a :: k), Ob (n :: v)) => ((Ob (n *. a)) => r) -> r
  copower :: (Ob (a :: k), Ob b) => n ~> HomObj v a b -> (n *. a) ~> b
  uncopower :: (Ob (a :: k), Ob n) => (n *. a) ~> b -> n ~> HomObj v a b

-- mapCobase :: forall {k} {v} (a :: k) b (n :: v). (Copowered v k, Ob n) => a ~> b -> n *. a ~> n *. b
-- mapCobase f = f // withObCopower @v @k @b @n (copower @v @k @a @(n *. b) @n (\n -> uncopower id n . f))

mapCopower :: forall {k} {v} (a :: k) (n :: v) m. (Copowered v k, Ob a) => (n ~> m) -> n *. a ~> m *. a
mapCopower :: forall {k} {v} (a :: k) (n :: v) (m :: v).
(Copowered v k, Ob a) =>
(n ~> m) -> (n *. a) ~> (m *. a)
mapCopower n ~> m
f = forall v k (a :: k) (n :: v) r.
(Copowered v k, Ob a, Ob n) =>
(Ob (n *. a) => r) -> r
withObCopower @v @k @a @m (forall v k (a :: k) (b :: k) (n :: v).
(Copowered v k, Ob a, Ob b) =>
(n ~> HomObj v a b) -> (n *. a) ~> b
copower @v @k @a @(m *. a) @n (forall v k (a :: k) (n :: v) (b :: k).
(Copowered v k, Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj v a b
uncopower @v @k @a (m *. a) ~> (m *. a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (m ~> HomObj v a (m *. a)) -> (n ~> m) -> n ~> HomObj v a (m *. a)
forall (b :: v) (c :: v) (a :: v). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. n ~> m
f)) ((Ob n, Ob m) => (n *. a) ~> (m *. a))
-> (n ~> m) -> (n *. a) ~> (m *. a)
forall (a :: v) (b :: v) r. ((Ob a, Ob b) => r) -> (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
\\ n ~> m
f

instance Copowered Type Type where
  type n *. a = (n, a)
  withObCopower :: forall a n r. (Ob a, Ob n) => (Ob (n *. a) => r) -> r
withObCopower Ob (n *. a) => r
r = r
Ob (n *. a) => r
r
  copower :: forall a b n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> (n *. a) ~> b
copower n ~> HomObj Type a b
f = \(n
n, a
a) -> n ~> HomObj Type a b
n -> (a -> b)
f n
n a
a
  uncopower :: forall a n b.
(Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj Type a b
uncopower (n *. a) ~> b
f n
n a
a = (n *. a) ~> b
(n, a) -> b
f (n
n, a
a)

instance Copowered Type () where
  type n *. a = '()
  withObCopower :: forall (a :: ()) n r. (Ob a, Ob n) => (Ob (n *. a) => r) -> r
withObCopower Ob (n *. a) => r
r = r
Ob (n *. a) => r
r
  copower :: forall (a :: ()) (b :: ()) n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> (n *. a) ~> b
copower n ~> HomObj Type a b
_ = (n *. a) ~> b
Unit '() '()
Unit
  uncopower :: forall (a :: ()) n (b :: ()).
(Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj Type a b
uncopower (n *. a) ~> b
Unit '() b
Unit n
_ = Unit '() b
Unit '() '()
Unit

instance (Copowered Type j, Copowered Type k) => Copowered Type (j, k) where
  type n *. '(a, b) = '(n *. a, n *. b)
  withObCopower :: forall (a :: (j, k)) n r. (Ob a, Ob n) => (Ob (n *. a) => r) -> r
withObCopower @'(a, b) @n Ob (n *. a) => r
r = forall v k (a :: k) (n :: v) r.
(Copowered v k, Ob a, Ob n) =>
(Ob (n *. a) => r) -> r
withObCopower @_ @j @a @n (forall v k (a :: k) (n :: v) r.
(Copowered v k, Ob a, Ob n) =>
(Ob (n *. a) => r) -> r
withObCopower @_ @k @b @n r
Ob (n *. Snd a) => r
Ob (n *. a) => r
r)
  copower :: forall (a :: (j, k)) (b :: (j, k)) n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> (n *. a) ~> b
copower n ~> HomObj Type a b
f = (n ~> HomObj Type (Fst a) (Fst b)) -> (n *. Fst a) ~> Fst b
forall (a :: j) (b :: j) n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> (n *. a) ~> b
forall v k (a :: k) (b :: k) (n :: v).
(Copowered v k, Ob a, Ob b) =>
(n ~> HomObj v a b) -> (n *. a) ~> b
copower (\n
n -> (:**:) (~>) (~>) '(Fst a, Snd a) '(Fst b, Snd b) -> Fst a ~> Fst b
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
(:**:) c d '(a1, a2) '(b1, b2) -> c a1 b1
fstK (n ~> HomObj Type a b
n -> (:**:) (~>) (~>) '(Fst a, Snd a) '(Fst b, Snd b)
f n
n)) ((n *. Fst a) ~> Fst b)
-> ((n *. Snd a) ~> Snd b)
-> (:**:) (~>) (~>) '(n *. Fst a, n *. Snd a) '(Fst b, Snd b)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (n ~> HomObj Type (Snd a) (Snd b)) -> (n *. Snd a) ~> Snd b
forall (a :: k) (b :: k) n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> (n *. a) ~> b
forall v k (a :: k) (b :: k) (n :: v).
(Copowered v k, Ob a, Ob b) =>
(n ~> HomObj v a b) -> (n *. a) ~> b
copower (\n
n -> (:**:) (~>) (~>) '(Fst a, Snd a) '(Fst b, Snd b) -> Snd a ~> Snd b
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
(:**:) c d '(a1, a2) '(b1, b2) -> d a2 b2
sndK (n ~> HomObj Type a b
n -> (:**:) (~>) (~>) '(Fst a, Snd a) '(Fst b, Snd b)
f n
n))
  uncopower :: forall (a :: (j, k)) n (b :: (j, k)).
(Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj Type a b
uncopower (a1 ~> b1
f :**: a2 ~> b2
g) n
n = ((n *. Fst a) ~> b1) -> n ~> HomObj Type (Fst a) b1
forall (a :: j) n (b :: j).
(Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj Type a b
forall v k (a :: k) (n :: v) (b :: k).
(Copowered v k, Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj v a b
uncopower a1 ~> b1
(n *. Fst a) ~> b1
f n
n (Fst a ~> b1)
-> (Snd a ~> b2) -> (:**:) (~>) (~>) '(Fst a, Snd a) '(b1, b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: ((n *. Snd a) ~> b2) -> n ~> HomObj Type (Snd a) b2
forall (a :: k) n (b :: k).
(Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj Type a b
forall v k (a :: k) (n :: v) (b :: k).
(Copowered v k, Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj v a b
uncopower a2 ~> b2
(n *. Snd a) ~> b2
g n
n

data (n :*.: p) a b where
  Copower :: n -> p a b -> (n :*.: p) a b
instance (Profunctor p) => Profunctor (n :*.: p) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> (:*.:) n p a b -> (:*.:) n p c d
dimap c ~> a
l b ~> d
r (Copower n
n p a b
p) = n -> p c d -> (:*.:) n p c d
forall {k} {k} n (p :: k -> k -> Type) (a :: k) (b :: k).
n -> p a b -> (:*.:) n p a b
Copower n
n ((c ~> a) -> (b ~> d) -> p a b -> p c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(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 c ~> a
l b ~> d
r p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> (:*.:) n p a b -> r
\\ Copower n
_ p a b
p = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: j) 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 (CategoryOf j, CategoryOf k) => Copowered Type (j +-> k) where
  type n *. a = n :*.: a
  withObCopower :: forall (a :: j +-> k) n r. (Ob a, Ob n) => (Ob (n *. a) => r) -> r
withObCopower Ob (n *. a) => r
r = r
Ob (n *. a) => r
r
  copower :: forall (a :: j +-> k) (b :: j +-> k) n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> (n *. a) ~> b
copower n ~> HomObj Type a b
f = ((n :*.: a) :~> b) -> Prof (n :*.: a) b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Copower n
n a a b
p) -> Prof a b -> a :~> b
forall {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
Prof p q -> p :~> q
unProf (n ~> HomObj Type a b
n -> Prof a b
f n
n) a a b
p
  uncopower :: forall (a :: j +-> k) n (b :: j +-> k).
(Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj Type a b
uncopower (Prof (n :*.: a) :~> b
f) n
n = (a :~> b) -> Prof a b
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \a a b
p -> (:*.:) n a a b -> b a b
(n :*.: a) :~> b
f (n -> a a b -> (:*.:) n a a b
forall {k} {k} n (p :: k -> k -> Type) (a :: k) (b :: k).
n -> p a b -> (:*.:) n p a b
Copower n
n a a b
p)

class (HomObj v (OP a) (OP b) ~ HomObj v b a) => HomObjOp v a b
instance (HomObj v (OP a) (OP b) ~ HomObj v b a) => HomObjOp v a b

instance (Copowered v k, Enriched v (OPPOSITE k), forall (a :: k) b. HomObjOp v a b) => Powered v (OPPOSITE k) where
  type OP a ^ n = OP (n *. a)
  withObPower :: forall (a :: OPPOSITE k) (n :: v) r.
(Ob a, Ob n) =>
(Ob (a ^ n) => r) -> r
withObPower @(OP a) @n Ob (a ^ n) => r
r = forall v k (a :: k) (n :: v) r.
(Copowered v k, Ob a, Ob n) =>
(Ob (n *. a) => r) -> r
withObCopower @v @k @a @n r
Ob (n *. UN 'OP a) => r
Ob (a ^ n) => r
r
  power :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (n :: v).
(Ob a, Ob b) =>
(n ~> HomObj v a b) -> a ~> (b ^ n)
power @(OP a) @(OP b) n ~> HomObj v a b
f = ((n *. UN 'OP b) ~> UN 'OP a)
-> Op (~>) ('OP (UN 'OP a)) ('OP (n *. UN 'OP b))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (forall v k (a :: k) (b :: k) (n :: v).
(Copowered v k, Ob a, Ob b) =>
(n ~> HomObj v a b) -> (n *. a) ~> b
copower @v @k @b @a n ~> ProObj v (~>) (UN 'OP b) (UN 'OP a)
n ~> HomObj v a b
f)
  unpower :: forall (b :: OPPOSITE k) (n :: v) (a :: OPPOSITE k).
(Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj v a b
unpower @(OP a) (Op b1 ~> a1
f) = forall v k (a :: k) (n :: v) (b :: k).
(Copowered v k, Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj v a b
uncopower @v @k @a b1 ~> a1
(n *. UN 'OP b) ~> a1
f

instance (Powered v k, Enriched v (OPPOSITE k), forall (a :: k) b. HomObjOp v a b) => Copowered v (OPPOSITE k) where
  type n *. OP a = OP (a ^ n)
  withObCopower :: forall (a :: OPPOSITE k) (n :: v) r.
(Ob a, Ob n) =>
(Ob (n *. a) => r) -> r
withObCopower @(OP a) @n Ob (n *. a) => r
r = forall v k (a :: k) (n :: v) r.
(Powered v k, Ob a, Ob n) =>
(Ob (a ^ n) => r) -> r
withObPower @v @k @a @n r
Ob (UN 'OP a ^ n) => r
Ob (n *. a) => r
r
  copower :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (n :: v).
(Ob a, Ob b) =>
(n ~> HomObj v a b) -> (n *. a) ~> b
copower @(OP a) @(OP b) n ~> HomObj v a b
f = (UN 'OP b ~> (UN 'OP a ^ n))
-> Op (~>) ('OP (UN 'OP a ^ n)) ('OP (UN 'OP b))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (forall v k (a :: k) (b :: k) (n :: v).
(Powered v k, Ob a, Ob b) =>
(n ~> HomObj v a b) -> a ~> (b ^ n)
power @v @k @b @a n ~> ProObj v (~>) (UN 'OP b) (UN 'OP a)
n ~> HomObj v a b
f)
  uncopower :: forall (a :: OPPOSITE k) (n :: v) (b :: OPPOSITE k).
(Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj v a b
uncopower @(OP a) (Op b1 ~> a1
f) = forall v k (b :: k) (n :: v) (a :: k).
(Powered v k, Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj v a b
unpower @v @k @a b1 ~> a1
b1 ~> (UN 'OP a ^ n)
f