module Proarrow.Category.Instance.Lifted (LIFTED (..), Lift (..), LIFTEDF, pattern LiftF) where

import Proarrow.Adjunction (Adjunction, unit')
import Proarrow.Category.Monoidal (MonoidalProfunctor (..))
import Proarrow.Core
import Proarrow.Functor (Functor)
import Proarrow.Object (pattern Obj)
import Proarrow.Object.BinaryCoproduct (Coprod, HasBinaryCoproducts (..), codiag, copar)
import Proarrow.Object.BinaryProduct (Cartesian, HasBinaryProducts (..), diag)
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Costar (Costar (..))
import Proarrow.Profunctor.Star (Star (..))

newtype LIFTED (p :: j +-> k) (q :: k +-> j) = LIFT j
type instance UN LIFT (LIFT j) = j

-- | A category lifted by an adjunction.
data Lift a b where
  Lift :: (q :.: p) a b -> Lift (LIFT a :: LIFTED p q) (LIFT b)

instance (Adjunction p q) => Profunctor (Lift :: CAT (LIFTED p q)) where
  dimap :: forall (c :: LIFTED p q) (a :: LIFTED p q) (b :: LIFTED p q)
       (d :: LIFTED p q).
(c ~> a) -> (b ~> d) -> Lift a b -> Lift c d
dimap = (c ~> a) -> (b ~> d) -> Lift a b -> Lift c d
Lift c a -> Lift b d -> Lift a b -> Lift 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 :: LIFTED p q) (b :: LIFTED p q) r.
((Ob a, Ob b) => r) -> Lift a b -> r
\\ Lift (:.:) q p a b
pq = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (:.:) q p a b -> r
forall (a :: j) (b :: j) r.
((Ob a, Ob b) => r) -> (:.:) q 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
\\ (:.:) q p a b
pq
instance (Adjunction p q) => Promonad (Lift :: CAT (LIFTED p q)) where
  id :: forall (a :: LIFTED p q). Ob a => Lift a a
id = (:.:) q p (UN 'LIFT a) (UN 'LIFT a)
-> Lift ('LIFT (UN 'LIFT a)) ('LIFT (UN 'LIFT a))
forall {j} {i} {k} {p :: i +-> k} {q :: k +-> i} (q :: j +-> i)
       (p :: i +-> j) (a :: i) (b :: i).
(:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
Lift (:.:) q p (UN 'LIFT a) (UN 'LIFT a)
forall (a :: j). Ob a => (:.:) q p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Lift (:.:) q p a b
f . :: forall (b :: LIFTED p q) (c :: LIFTED p q) (a :: LIFTED p q).
Lift b c -> Lift a b -> Lift a c
. Lift (:.:) q p a b
g = (:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
forall {j} {i} {k} {p :: i +-> k} {q :: k +-> i} (q :: j +-> i)
       (p :: i +-> j) (a :: i) (b :: i).
(:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
Lift ((:.:) q p a b
f (:.:) q p a b -> (:.:) q p a a -> (:.:) q p a b
forall (b :: j) (c :: j) (a :: j).
(:.:) q p b c -> (:.:) q p a b -> (:.:) q 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
. (:.:) q p a a
(:.:) q p a b
g)
instance (Adjunction p q) => CategoryOf (LIFTED p q) where
  type (~>) = Lift
  type Ob (a :: LIFTED p q) = (Is LIFT a, Ob (UN LIFT a))

instance (Adjunction (p :: j +-> k) (q :: k +-> j), HasTerminalObject j) => HasTerminalObject (LIFTED p q) where
  type TerminalObject = LIFT TerminalObject
  terminate :: forall (a :: LIFTED p q). Ob a => a ~> TerminalObject
terminate = (:.:) q p (UN 'LIFT a) TerminalObject
-> Lift ('LIFT (UN 'LIFT a)) ('LIFT TerminalObject)
forall {j} {i} {k} {p :: i +-> k} {q :: k +-> i} (q :: j +-> i)
       (p :: i +-> j) (a :: i) (b :: i).
(:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
Lift ((UN 'LIFT a ~> TerminalObject)
-> (:.:) q p (UN 'LIFT a) TerminalObject
forall {i} {j} (p :: i +-> j) (q :: j +-> i) (a :: i) (b :: i).
Adjunction p q =>
(a ~> b) -> (:.:) q p a b
unit' UN 'LIFT a ~> TerminalObject
forall (a :: j). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate)

instance
  (Adjunction (p :: j +-> k) (q :: k +-> j), MonoidalProfunctor p, MonoidalProfunctor q, Cartesian j)
  => HasBinaryProducts (LIFTED p q)
  where
  type LIFT a && LIFT b = LIFT (a && b)
  withObProd :: forall (a :: LIFTED p q) (b :: LIFTED p q) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(LIFT a) @(LIFT b) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @j @a @b
  fst :: forall (a :: LIFTED p q) (b :: LIFTED p q).
(Ob a, Ob b) =>
(a && b) ~> a
fst @(LIFT a) @(LIFT b) = (:.:) q p (UN 'LIFT a && UN 'LIFT b) (UN 'LIFT a)
-> Lift ('LIFT (UN 'LIFT a && UN 'LIFT b)) ('LIFT (UN 'LIFT a))
forall {j} {i} {k} {p :: i +-> k} {q :: k +-> i} (q :: j +-> i)
       (p :: i +-> j) (a :: i) (b :: i).
(:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
Lift (((UN 'LIFT a && UN 'LIFT b) ~> UN 'LIFT a)
-> (:.:) q p (UN 'LIFT a && UN 'LIFT b) (UN 'LIFT a)
forall {i} {j} (p :: i +-> j) (q :: j +-> i) (a :: i) (b :: i).
Adjunction p q =>
(a ~> b) -> (:.:) q p a b
unit' (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @j @a @b))
  snd :: forall (a :: LIFTED p q) (b :: LIFTED p q).
(Ob a, Ob b) =>
(a && b) ~> b
snd @(LIFT a) @(LIFT b) = (:.:) q p (UN 'LIFT a && UN 'LIFT b) (UN 'LIFT b)
-> Lift ('LIFT (UN 'LIFT a && UN 'LIFT b)) ('LIFT (UN 'LIFT b))
forall {j} {i} {k} {p :: i +-> k} {q :: k +-> i} (q :: j +-> i)
       (p :: i +-> j) (a :: i) (b :: i).
(:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
Lift (((UN 'LIFT a && UN 'LIFT b) ~> UN 'LIFT b)
-> (:.:) q p (UN 'LIFT a && UN 'LIFT b) (UN 'LIFT b)
forall {i} {j} (p :: i +-> j) (q :: j +-> i) (a :: i) (b :: i).
Adjunction p q =>
(a ~> b) -> (:.:) q p a b
unit' (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @j @a @b))
  Lift (q a b
ql :.: p b b
pl) &&& :: forall (a :: LIFTED p q) (x :: LIFTED p q) (y :: LIFTED p q).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Lift (q a b
qr :.: p b b
pr) = (:.:) q p a (b && b) -> Lift ('LIFT a) ('LIFT (b && b))
forall {j} {i} {k} {p :: i +-> k} {q :: k +-> i} (q :: j +-> i)
       (p :: i +-> j) (a :: i) (b :: i).
(:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
Lift ((a ~> (a && a)) -> q (a && a) (b ** b) -> q a (b ** b)
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag (q a b
ql q a b -> q a b -> q (a ** a) (b ** b)
forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
q x1 x2 -> q y1 y2 -> q (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` q a b
q a b
qr) q a (b ** b) -> p (b ** b) (b && b) -> (:.:) q p a (b && b)
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (p b b
pl p b b -> p b b -> p (b ** b) (b ** b)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
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 b b
pr)) ((Ob a, Ob b) => Lift ('LIFT a) ('LIFT (b && b)))
-> q a b -> Lift ('LIFT a) ('LIFT (b && b))
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> q 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
\\ q a b
ql

instance (Adjunction (p :: j +-> k) (q :: k +-> j), HasInitialObject j) => HasInitialObject (LIFTED p q) where
  type InitialObject = LIFT InitialObject
  initiate :: forall (a :: LIFTED p q). Ob a => InitialObject ~> a
initiate = (:.:) q p InitialObject (UN 'LIFT a)
-> Lift ('LIFT InitialObject) ('LIFT (UN 'LIFT a))
forall {j} {i} {k} {p :: i +-> k} {q :: k +-> i} (q :: j +-> i)
       (p :: i +-> j) (a :: i) (b :: i).
(:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
Lift ((InitialObject ~> UN 'LIFT a)
-> (:.:) q p InitialObject (UN 'LIFT a)
forall {i} {j} (p :: i +-> j) (q :: j +-> i) (a :: i) (b :: i).
Adjunction p q =>
(a ~> b) -> (:.:) q p a b
unit' InitialObject ~> UN 'LIFT a
forall (a :: j). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate)

instance
  ( Adjunction (p :: j +-> k) (q :: k +-> j)
  , MonoidalProfunctor (Coprod p)
  , MonoidalProfunctor (Coprod q)
  , HasBinaryCoproducts j
  )
  => HasBinaryCoproducts (LIFTED p q)
  where
  type LIFT a || LIFT b = LIFT (a || b)
  withObCoprod :: forall (a :: LIFTED p q) (b :: LIFTED p q) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(LIFT a) @(LIFT b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @j @a @b
  lft :: forall (a :: LIFTED p q) (b :: LIFTED p q).
(Ob a, Ob b) =>
a ~> (a || b)
lft @(LIFT a) @(LIFT b) = (:.:) q p (UN 'LIFT a) (UN 'LIFT a || UN 'LIFT b)
-> Lift ('LIFT (UN 'LIFT a)) ('LIFT (UN 'LIFT a || UN 'LIFT b))
forall {j} {i} {k} {p :: i +-> k} {q :: k +-> i} (q :: j +-> i)
       (p :: i +-> j) (a :: i) (b :: i).
(:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
Lift ((UN 'LIFT a ~> (UN 'LIFT a || UN 'LIFT b))
-> (:.:) q p (UN 'LIFT a) (UN 'LIFT a || UN 'LIFT b)
forall {i} {j} (p :: i +-> j) (q :: j +-> i) (a :: i) (b :: i).
Adjunction p q =>
(a ~> b) -> (:.:) q p a b
unit' (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @j @a @b))
  rgt :: forall (a :: LIFTED p q) (b :: LIFTED p q).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @(LIFT a) @(LIFT b) = (:.:) q p (UN 'LIFT b) (UN 'LIFT a || UN 'LIFT b)
-> Lift ('LIFT (UN 'LIFT b)) ('LIFT (UN 'LIFT a || UN 'LIFT b))
forall {j} {i} {k} {p :: i +-> k} {q :: k +-> i} (q :: j +-> i)
       (p :: i +-> j) (a :: i) (b :: i).
(:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
Lift ((UN 'LIFT b ~> (UN 'LIFT a || UN 'LIFT b))
-> (:.:) q p (UN 'LIFT b) (UN 'LIFT a || UN 'LIFT b)
forall {i} {j} (p :: i +-> j) (q :: j +-> i) (a :: i) (b :: i).
Adjunction p q =>
(a ~> b) -> (:.:) q p a b
unit' (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @j @a @b))
  Lift (q a b
ql :.: p b b
pl) ||| :: forall (x :: LIFTED p q) (a :: LIFTED p q) (y :: LIFTED p q).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Lift (q a b
qr :.: p b b
pr) = (:.:) q p (a || a) b -> Lift ('LIFT (a || a)) ('LIFT b)
forall {j} {i} {k} {p :: i +-> k} {q :: k +-> i} (q :: j +-> i)
       (p :: i +-> j) (a :: i) (b :: i).
(:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
Lift ((q a b
ql q a b -> q a b -> q (a || a) (b || b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
`copar` q a b
qr) q (a || a) (b || b) -> p (b || b) b -> (:.:) q p (a || a) b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ((b || b) ~> b) -> p (b || b) (b || b) -> p (b || b) b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (b || b) ~> b
forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag (p b b
pl p b b -> p b b -> p (b || b) (b || b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
`copar` p b b
p b b
pr)) ((Ob b, Ob b) => Lift ('LIFT (a || a)) ('LIFT b))
-> p b b -> Lift ('LIFT (a || a)) ('LIFT b)
forall (a :: k) (b :: j) 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 b b
pl

-- | Categories lifted by a functor: @f a ~> f b@.
type LIFTEDF (f :: j -> k) = LIFTED (Star f) (Costar f)

unlift :: (Functor f) => Lift (LIFT a :: LIFTEDF f) (LIFT b) -> (f a ~> f b, Obj a, Obj b)
unlift :: forall {k} {k} {k} {p :: k +-> k} {q :: k +-> k} (f :: k -> k)
       (a :: k) (b :: k).
Functor f =>
Lift ('LIFT a) ('LIFT b) -> (f a ~> f b, Obj a, Obj b)
unlift (Lift (Costar f a ~> b
f :.: Star b ~> f b
g)) = (b ~> f b
b ~> f b
g (b ~> f b) -> (f a ~> b) -> f a ~> f 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
. f a ~> b
f a ~> b
f, Obj a
forall k (a :: k). (CategoryOf k, Ob a) => Obj a
Obj, Obj b
forall k (a :: k). (CategoryOf k, Ob a) => Obj a
Obj)

pattern LiftF :: (Functor f) => (Ob a, Ob b) => (f a ~> f b) -> Lift (LIFT a :: LIFTEDF f) (LIFT b)
pattern $mLiftF :: forall {r} {j1} {j2} {k} {p :: j1 +-> k} {q :: k +-> j1}
       {f :: j1 -> j2} {a :: j1} {b :: j1}.
Functor f =>
Lift ('LIFT a) ('LIFT b)
-> ((Ob a, Ob b) => (f a ~> f b) -> r) -> ((# #) -> r) -> r
$bLiftF :: forall {j1} {j2} {k} {p :: j1 +-> k} {q :: k +-> j1}
       (f :: j1 -> j2) (a :: j1) (b :: j1).
(Functor f, Ob a, Ob b) =>
(f a ~> f b) -> Lift ('LIFT a) ('LIFT b)
LiftF f <- (unlift -> (f, Obj, Obj))
  where
    LiftF f a ~> f b
f = (:.:) (Costar f) (Star f) a b -> Lift ('LIFT a) ('LIFT b)
forall {j} {i} {k} {p :: i +-> k} {q :: k +-> i} (q :: j +-> i)
       (p :: i +-> j) (a :: i) (b :: i).
(:.:) q p a b -> Lift ('LIFT a) ('LIFT b)
Lift ((f a ~> f b) -> Costar f a (f b)
forall {j} {k} (a :: j) (f :: j -> k) (b :: k).
Ob a =>
(f a ~> b) -> Costar f a b
Costar f a ~> f b
f Costar f a (f b) -> Star f (f b) b -> (:.:) (Costar f) (Star f) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (f b ~> f b) -> Star f (f b) b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star f b ~> f b
forall (a :: j2). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)

{-# COMPLETE LiftF #-}