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

-- | The 'Adj' newtype marks a profunctor as the heteromorphism profunctor of an adjunction: because left
-- adjoints preserve colimits and right adjoints preserve limits, @Adj p@ is a distributive monoidal
-- profunctor. Also proves that every adjunction between Hask endofunctors is equivalent to the
-- curry\/uncurry adjunction ('haskAdjIsCurryAdj').
module Proarrow.Profunctor.Instance.Adj where

import Data.Kind (Type)
import Prelude (const)

import Proarrow.Adjunction (Adjunction)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Colimit.BinaryCoproduct (Coprod (..), HasBinaryCoproducts (..), HasCoproducts)
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core (Profunctor (..), Promonad (..), lmap, rmap, type (+->))
import Proarrow.Limit.BinaryProduct (Cartesian, HasBinaryProducts (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Object (pattern Objs)
import Proarrow.Optic (PIso, iso)
import Proarrow.Optic.Getter (review, view)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), corepObj)
import Proarrow.Profunctor.Representable (Representable (..), repObj)

-- | Preservation of limits and colimits makes the adjunction heteromorphism a distributive profunctor.
newtype Adj p a b = Adj (p a b)
  deriving newtype (CategoryOf k
CategoryOf j
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a) -> (b ~> d) -> Adj p a b -> Adj p c d)
-> (forall (c :: k) (a :: k) (b :: j).
    (c ~> a) -> Adj p a b -> Adj p c b)
-> (forall (b :: j) (d :: j) (a :: k).
    (b ~> d) -> Adj p a b -> Adj p a d)
-> (forall (a :: k) (b :: j) r.
    ((Ob a, Ob b) => r) -> Adj p a b -> r)
-> Profunctor (Adj p)
forall (c :: k) (a :: k) (b :: j).
(c ~> a) -> Adj p a b -> Adj p c b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Adj p a b -> Adj p c d
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Adj p a b -> r
forall (b :: j) (d :: j) (a :: k).
(b ~> d) -> Adj p a b -> Adj p a d
forall k j (p :: k -> j -> Type). Profunctor p => CategoryOf k
forall k j (p :: k -> j -> Type). Profunctor p => CategoryOf j
forall k j (p :: k -> j -> Type) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> Adj p a b -> Adj p c b
forall k j (p :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> Adj p a b -> Adj p c d
forall k j (p :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> Adj p a b -> r
forall k j (p :: k -> j -> Type) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> Adj p a b -> Adj p a d
forall {j} {k} (p :: j +-> k).
(CategoryOf j, CategoryOf k) =>
(forall (c :: k) (a :: k) (b :: j) (d :: j).
 (c ~> a) -> (b ~> d) -> p a b -> p c d)
-> (forall (c :: k) (a :: k) (b :: j). (c ~> a) -> p a b -> p c b)
-> (forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d)
-> (forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r)
-> Profunctor p
$cdimap :: forall k j (p :: k -> j -> Type) (c :: k) (a :: k) (b :: j)
       (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> Adj p a b -> Adj p c d
dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Adj p a b -> Adj p c d
$clmap :: forall k j (p :: k -> j -> Type) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> Adj p a b -> Adj p c b
lmap :: forall (c :: k) (a :: k) (b :: j).
(c ~> a) -> Adj p a b -> Adj p c b
$crmap :: forall k j (p :: k -> j -> Type) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> Adj p a b -> Adj p a d
rmap :: forall (b :: j) (d :: j) (a :: k).
(b ~> d) -> Adj p a b -> Adj p a d
$c\\ :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> Adj p a b -> r
\\ :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> Adj p a b -> r
Profunctor, Profunctor (Adj p)
Profunctor (Adj p) =>
(forall (a :: k) (b :: j). Adj p a b -> a ~> (Adj p % b))
-> (forall (b :: j) (a :: k).
    Ob b =>
    (a ~> (Adj p % b)) -> Adj p a b)
-> (forall (a :: j) (b :: j).
    (a ~> b) -> (Adj p % a) ~> (Adj p % b))
-> (forall (a :: j). Ob a => Adj p (Adj p % a) a)
-> Representable (Adj p)
forall (a :: k) (b :: j). Adj p a b -> a ~> (Adj p % b)
forall (a :: j). Ob a => Adj p (Adj p % a) a
forall (b :: j) (a :: k). Ob b => (a ~> (Adj p % b)) -> Adj p a b
forall (a :: j) (b :: j). (a ~> b) -> (Adj p % a) ~> (Adj p % b)
forall k j (p :: k -> j -> Type).
Representable p =>
Profunctor (Adj p)
forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
Representable p =>
Adj p a b -> a ~> (Adj p % b)
forall k j (p :: k -> j -> Type) (a :: j).
(Representable p, Ob a) =>
Adj p (Adj p % a) a
forall k j (p :: k -> j -> Type) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (Adj p % b)) -> Adj p a b
forall k j (p :: k -> j -> Type) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (Adj p % a) ~> (Adj p % b)
forall {j} {k} (p :: j +-> k).
Profunctor p =>
(forall (a :: k) (b :: j). p a b -> a ~> (p % b))
-> (forall (b :: j) (a :: k). Ob b => (a ~> (p % b)) -> p a b)
-> (forall (a :: j) (b :: j). (a ~> b) -> (p % a) ~> (p % b))
-> (forall (a :: j). Ob a => p (p % a) a)
-> Representable p
$cindex :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
Representable p =>
Adj p a b -> a ~> (Adj p % b)
index :: forall (a :: k) (b :: j). Adj p a b -> a ~> (Adj p % b)
$ctabulate :: forall k j (p :: k -> j -> Type) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (Adj p % b)) -> Adj p a b
tabulate :: forall (b :: j) (a :: k). Ob b => (a ~> (Adj p % b)) -> Adj p a b
$crepMap :: forall k j (p :: k -> j -> Type) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (Adj p % a) ~> (Adj p % b)
repMap :: forall (a :: j) (b :: j). (a ~> b) -> (Adj p % a) ~> (Adj p % b)
$crepUniv :: forall k j (p :: k -> j -> Type) (a :: j).
(Representable p, Ob a) =>
Adj p (Adj p % a) a
repUniv :: forall (a :: j). Ob a => Adj p (Adj p % a) a
Representable, Profunctor (Adj p)
Profunctor (Adj p) =>
(forall (a :: k) (b :: j). Adj p a b -> (Adj p %% a) ~> b)
-> (forall (a :: k) (b :: j).
    Ob a =>
    ((Adj p %% a) ~> b) -> Adj p a b)
-> (forall (a :: k) (b :: k).
    (a ~> b) -> (Adj p %% a) ~> (Adj p %% b))
-> (forall (a :: k). Ob a => Adj p a (Adj p %% a))
-> Corepresentable (Adj p)
forall (a :: k). Ob a => Adj p a (Adj p %% a)
forall (a :: k) (b :: k). (a ~> b) -> (Adj p %% a) ~> (Adj p %% b)
forall (a :: k) (b :: j). Ob a => ((Adj p %% a) ~> b) -> Adj p a b
forall (a :: k) (b :: j). Adj p a b -> (Adj p %% a) ~> b
forall k j (p :: k -> j -> Type).
Corepresentable p =>
Profunctor (Adj p)
forall k j (p :: k -> j -> Type) (a :: k).
(Corepresentable p, Ob a) =>
Adj p a (Adj p %% a)
forall k j (p :: k -> j -> Type) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (Adj p %% a) ~> (Adj p %% b)
forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((Adj p %% a) ~> b) -> Adj p a b
forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
Corepresentable p =>
Adj p a b -> (Adj p %% a) ~> b
forall {j} {k} (p :: j +-> k).
Profunctor p =>
(forall (a :: k) (b :: j). p a b -> (p %% a) ~> b)
-> (forall (a :: k) (b :: j). Ob a => ((p %% a) ~> b) -> p a b)
-> (forall (a :: k) (b :: k). (a ~> b) -> (p %% a) ~> (p %% b))
-> (forall (a :: k). Ob a => p a (p %% a))
-> Corepresentable p
$ccoindex :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
Corepresentable p =>
Adj p a b -> (Adj p %% a) ~> b
coindex :: forall (a :: k) (b :: j). Adj p a b -> (Adj p %% a) ~> b
$ccotabulate :: forall k j (p :: k -> j -> Type) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((Adj p %% a) ~> b) -> Adj p a b
cotabulate :: forall (a :: k) (b :: j). Ob a => ((Adj p %% a) ~> b) -> Adj p a b
$ccorepMap :: forall k j (p :: k -> j -> Type) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (Adj p %% a) ~> (Adj p %% b)
corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Adj p %% a) ~> (Adj p %% b)
$ccorepUniv :: forall k j (p :: k -> j -> Type) (a :: k).
(Corepresentable p, Ob a) =>
Adj p a (Adj p %% a)
corepUniv :: forall (a :: k). Ob a => Adj p a (Adj p %% a)
Corepresentable)

instance (Cartesian j, Cartesian k, Corepresentable p) => MonoidalProfunctor (Adj p :: j +-> k) where
  one :: Adj p Unit Unit
one = ((Adj p %% TerminalObject) ~> TerminalObject)
-> Adj p TerminalObject TerminalObject
forall (a :: k) (b :: j). Ob a => ((Adj p %% a) ~> b) -> Adj p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate (p %% TerminalObject) ~> TerminalObject
(Adj p %% TerminalObject) ~> TerminalObject
forall (a :: j). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate ((Ob (p %% TerminalObject), Ob (p %% TerminalObject)) =>
 Adj p TerminalObject TerminalObject)
-> ((p %% TerminalObject) ~> (p %% TerminalObject))
-> Adj p TerminalObject TerminalObject
forall (a :: j) (b :: j) 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
\\ forall {k1} {k2} (p :: k1 +-> k2) (a :: k2).
(Corepresentable p, Ob a) =>
Obj (p %% a)
forall (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
Obj (p %% a)
corepObj @p @TerminalObject
  Adj @_ @x l :: p x1 x2
l@p x1 x2
Objs ** :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
Adj p x1 x2 -> Adj p y1 y2 -> Adj p (x1 ** y1) (x2 ** y2)
** Adj @_ @y r :: p y1 y2
r@p y1 y2
Objs =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @y
      ( ((Adj p %% (x1 ** y1)) ~> (x2 ** y2))
-> Adj p (x1 ** y1) (x2 ** y2)
forall (a :: k) (b :: j). Ob a => ((Adj p %% a) ~> b) -> Adj p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate
          ( forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex @p @(x ** y) (((x1 ** y1) ~> x1) -> p x1 x2 -> p (x1 ** y1) x2
forall (c :: k) (a :: k) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @x @y) p x1 x2
l)
              ((p %% (x1 ** y1)) ~> x2)
-> ((p %% (x1 ** y1)) ~> y2) -> (p %% (x1 ** y1)) ~> (x2 && y2)
forall (a :: j) (x :: j) (y :: j).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex @p @(x ** y) (((x1 ** y1) ~> y1) -> p y1 y2 -> p (x1 ** y1) y2
forall (c :: k) (a :: k) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @x @y) p y1 y2
r)
          )
      )

instance (HasCoproducts j, HasCoproducts k, Representable p) => MonoidalProfunctor (Coprod (Adj p :: j +-> k)) where
  one :: Coprod (Adj p) Unit Unit
one = ('COPR InitialObject ~> (Coprod (Adj p) % 'COPR InitialObject))
-> Coprod (Adj p) ('COPR InitialObject) ('COPR InitialObject)
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
forall (b :: COPROD j) (a :: COPROD k).
Ob b =>
(a ~> (Coprod (Adj p) % b)) -> Coprod (Adj p) a b
tabulate InitialObject ~> 'COPR (p % InitialObject)
'COPR InitialObject ~> (Coprod (Adj p) % 'COPR InitialObject)
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
forall (a :: COPROD k). Ob a => InitialObject ~> a
initiate ((Ob (p % InitialObject), Ob (p % InitialObject)) =>
 Coprod (Adj p) ('COPR InitialObject) ('COPR InitialObject))
-> ((p % InitialObject) ~> (p % InitialObject))
-> Coprod (Adj p) ('COPR InitialObject) ('COPR InitialObject)
forall (a :: k) (b :: k) 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
\\ forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
forall (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
Obj (p % a)
repObj @p @InitialObject
  Coprod (Adj @_ @_ @x l :: p a1 b1
l@p a1 b1
Objs) ** :: forall (x1 :: COPROD k) (x2 :: COPROD j) (y1 :: COPROD k)
       (y2 :: COPROD j).
Coprod (Adj p) x1 x2
-> Coprod (Adj p) y1 y2 -> Coprod (Adj p) (x1 ** y1) (x2 ** y2)
** Coprod (Adj @_ @_ @y r :: p a1 b1
r@p a1 b1
Objs) =
    forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @x @y
      ( Adj p (a1 || a1) (b1 || b1)
-> Coprod (Adj p) ('COPR (a1 || a1)) ('COPR (b1 || b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod
          ( p (a1 || a1) (b1 || b1) -> Adj p (a1 || a1) (b1 || b1)
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> Adj p a b
Adj
              ( ((a1 || a1) ~> (p % (b1 || b1))) -> p (a1 || a1) (b1 || b1)
forall (b :: j) (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
                  ( forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index @p @_ @(x || y) ((b1 ~> (b1 || b1)) -> p a1 b1 -> p a1 (b1 || b1)
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @x @y) p a1 b1
l)
                      (a1 ~> (p % (b1 || b1)))
-> (a1 ~> (p % (b1 || b1))) -> (a1 || a1) ~> (p % (b1 || b1))
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index @p @_ @(x || y) ((b1 ~> (b1 || b1)) -> p a1 b1 -> p a1 (b1 || b1)
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @x @y) p a1 b1
r)
                  )
              )
          )
      )

-- | Every adjunction between Hask endofunctors is equivalent to the curry-uncurry adjunction.
haskAdjIsCurryAdj
  :: forall p a b a' b'
   . (Adjunction (p :: Type +-> Type)) => PIso (p %% () -> a -> b) (p %% () -> a' -> b') (p a b) (p a' b')
haskAdjIsCurryAdj :: forall (p :: Type +-> Type) a b a' b'.
Adjunction p =>
PIso
  ((p %% ()) -> a -> b) ((p %% ()) -> a' -> b') (p a b) (p a' b')
haskAdjIsCurryAdj =
  (((p %% ()) -> a -> b) ~> p a b)
-> (p a' b' ~> ((p %% ()) -> a' -> b'))
-> Optic_
     (OPT (p a b) (p a' b'))
     (OPT ((p %% ()) -> a -> b) ((p %% ()) -> a' -> b'))
forall {j} {k} (c :: (j +-> k) -> Constraint) (s :: k) (t :: j)
       (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, IsOptic c) =>
(s ~> a) -> (b ~> t) -> Optic c s t a b
iso (\(p %% ()) -> a -> b
kab -> (a ~> (p % b)) -> p a b
forall b a. 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
a -> forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: Type +-> Type) a b.
Representable p =>
p a b -> a ~> (p % b)
index @p (((p %% ()) ~> b) -> p () b
forall a b. Ob a => ((p %% a) ~> b) -> p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate ((p %% ()) -> a -> b
`kab` a
a)) ()) (\p a' b'
p p %% ()
k a'
a -> p a' b' -> (p %% a') ~> b'
forall a b. p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex p a' b'
p (forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: Type +-> Type) a b.
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @p (\() -> a'
a) p %% ()
k))

instance (Adjunction p) => Promonad (Adj p :: Type +-> Type) where
  id :: forall a. Ob a => Adj p a a
id = p a a -> Adj p a a
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> Adj p a b
Adj (Optic
  Profunctor
  ((p %% ()) -> a -> a)
  ((p %% ()) -> ZonkAny 0 -> ZonkAny 1)
  (p a a)
  (p (ZonkAny 0) (ZonkAny 1))
-> ((p %% ()) -> a -> a) ~> p a a
forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob a => c (Rep (Constant a))) =>
Optic c s t a b -> s ~> a
view (forall (p :: Type +-> Type) a b a' b'.
Adjunction p =>
PIso
  ((p %% ()) -> a -> b) ((p %% ()) -> a' -> b') (p a b) (p a' b')
haskAdjIsCurryAdj @p) ((a -> a) -> (p %% ()) -> a -> a
forall a b. a -> b -> a
const a -> a
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id))
  Adj p b c
l . :: forall b c a. Adj p b c -> Adj p a b -> Adj p a c
. Adj p a b
r = p a c -> Adj p a c
forall {k} {k} (p :: k -> k -> Type) (a :: k) (b :: k).
p a b -> Adj p a b
Adj (Optic
  Profunctor
  ((p %% ()) -> a -> c)
  ((p %% ()) -> ZonkAny 2 -> ZonkAny 3)
  (p a c)
  (p (ZonkAny 2) (ZonkAny 3))
-> ((p %% ()) -> a -> c) ~> p a c
forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob a => c (Rep (Constant a))) =>
Optic c s t a b -> s ~> a
view (forall (p :: Type +-> Type) a b a' b'.
Adjunction p =>
PIso
  ((p %% ()) -> a -> b) ((p %% ()) -> a' -> b') (p a b) (p a' b')
haskAdjIsCurryAdj @p) (\p %% ()
k -> Optic
  Profunctor
  ((p %% ()) -> ZonkAny 4 -> ZonkAny 5)
  ((p %% ()) -> b -> c)
  (p (ZonkAny 4) (ZonkAny 5))
  (p b c)
-> p b c ~> ((p %% ()) -> b -> c)
forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob b => c (Corep (Constant b))) =>
Optic c s t a b -> b ~> t
review Optic
  Profunctor
  ((p %% ()) -> ZonkAny 4 -> ZonkAny 5)
  ((p %% ()) -> b -> c)
  (p (ZonkAny 4) (ZonkAny 5))
  (p b c)
forall (p :: Type +-> Type) a b a' b'.
Adjunction p =>
PIso
  ((p %% ()) -> a -> b) ((p %% ()) -> a' -> b') (p a b) (p a' b')
haskAdjIsCurryAdj p b c
l p %% ()
k (b -> c) -> (a -> b) -> a -> c
forall b c a. (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
. Optic
  Profunctor
  ((p %% ()) -> ZonkAny 6 -> ZonkAny 7)
  ((p %% ()) -> a -> b)
  (p (ZonkAny 6) (ZonkAny 7))
  (p a b)
-> p a b ~> ((p %% ()) -> a -> b)
forall {j} {k} (c :: (k -> j -> Type) -> Constraint) (s :: k)
       (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob b => c (Corep (Constant b))) =>
Optic c s t a b -> b ~> t
review Optic
  Profunctor
  ((p %% ()) -> ZonkAny 6 -> ZonkAny 7)
  ((p %% ()) -> a -> b)
  (p (ZonkAny 6) (ZonkAny 7))
  (p a b)
forall (p :: Type +-> Type) a b a' b'.
Adjunction p =>
PIso
  ((p %% ()) -> a -> b) ((p %% ()) -> a' -> b') (p a b) (p a' b')
haskAdjIsCurryAdj p a b
r p %% ()
k))