{-# OPTIONS_GHC -Wno-orphans #-}
module Proarrow.Category.Instance.Nat where

import Data.Kind (Type)
import Data.Functor.Identity (Identity (..))
import Data.Functor.Compose (Compose (..))

import Proarrow.Core (CAT, CategoryOf (..), Promonad (..), Profunctor (..), Is, UN, dimapDefault)
import Proarrow.Functor (Functor (..), type (.~>))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))

type Nat :: CAT (j -> k)
data Nat f g where
  Nat :: (Functor f, Functor g)
      => { forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g
getNat :: f .~> g }
      -> Nat f g

instance CategoryOf (k1 -> Type) where
  type instance (~>) = Nat
  type Ob f = Functor f

instance Promonad (Nat :: CAT (j -> Type)) where
  id :: forall (a :: j -> Type). Ob a => Nat a a
id = Nat a a
forall {j} {k} (f :: j -> k). Functor f => Nat f f
n where
    n :: forall f. Functor f => Nat f f
    n :: forall {j} {k} (f :: j -> k). Functor f => Nat f f
n = (f .~> f) -> Nat f f
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (f :: j -> k) (a :: j) (b :: j).
Functor f =>
(a ~> b) -> f a ~> f b
map @f a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Nat b .~> c
f . :: forall (b :: j -> Type) (c :: j -> Type) (a :: j -> Type).
Nat b c -> Nat a b -> Nat a c
. Nat a .~> b
g = (a .~> c) -> Nat a c
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (b a ~> c a
b a -> c a
b .~> c
f (b a -> c a) -> (a a -> b a) -> a a -> c a
forall b c a. (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 ~> b a
a a -> b a
a .~> b
g)

instance Profunctor (Nat :: CAT (k1 -> Type)) where
  dimap :: forall (c :: k1 -> Type) (a :: k1 -> Type) (b :: k1 -> Type)
       (d :: k1 -> Type).
(c ~> a) -> (b ~> d) -> Nat a b -> Nat c d
dimap = (c ~> a) -> (b ~> d) -> Nat a b -> Nat c d
Nat c a -> Nat b d -> Nat a b -> Nat 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 :: k1 -> Type) (b :: k1 -> Type) r.
((Ob a, Ob b) => r) -> Nat a b -> r
\\ Nat{} = r
(Ob a, Ob b) => r
r

instance Monoidal (Type -> Type) where
  type Unit = Identity
  type f ** g = Compose f g
  Nat a .~> b
n par :: forall (a :: Type -> Type) (b :: Type -> Type) (c :: Type -> Type)
       (d :: Type -> Type).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
`par` Nat c .~> d
m = (Compose a c .~> Compose b d) -> Nat (Compose a c) (Compose b d)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (\(Compose a (c a)
fg) -> b (d a) -> Compose b d a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (a (d a) ~> b (d a)
a (d a) -> b (d a)
a .~> b
n ((c a ~> d a) -> a (c a) ~> a (d a)
forall a b. (a ~> b) -> a a ~> a b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map c a ~> d a
c .~> d
m a (c a)
fg)))
  leftUnitor :: forall (a :: Type -> Type). Obj a -> (Unit ** a) ~> a
leftUnitor Nat{} = (Compose Identity a .~> a) -> Nat (Compose Identity a) a
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (Identity (a a) -> a a
forall a. Identity a -> a
runIdentity (Identity (a a) -> a a)
-> (Compose Identity a a -> Identity (a a))
-> Compose Identity a a
-> a a
forall b c a. (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
. Compose Identity a a -> Identity (a a)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
  leftUnitorInv :: forall (a :: Type -> Type). Obj a -> a ~> (Unit ** a)
leftUnitorInv Nat{} = (a .~> Compose Identity a) -> Nat a (Compose Identity a)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (Identity (a a) -> Compose Identity a a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Identity (a a) -> Compose Identity a a)
-> (a a -> Identity (a a)) -> a a -> Compose Identity a a
forall b c a. (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 -> Identity (a a)
forall a. a -> Identity a
Identity)
  rightUnitor :: forall (a :: Type -> Type). Obj a -> (a ** Unit) ~> a
rightUnitor Nat{} = (Compose a Identity .~> a) -> Nat (Compose a Identity) a
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat ((Identity a ~> a) -> a (Identity a) ~> a a
forall a b. (a ~> b) -> a a ~> a b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map Identity a ~> a
Identity a -> a
forall a. Identity a -> a
runIdentity (a (Identity a) -> a a)
-> (Compose a Identity a -> a (Identity a))
-> Compose a Identity a
-> a a
forall b c a. (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
. Compose a Identity a -> a (Identity a)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
  rightUnitorInv :: forall (a :: Type -> Type). Obj a -> a ~> (a ** Unit)
rightUnitorInv Nat{} = (a .~> Compose a Identity) -> Nat a (Compose a Identity)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (a (Identity a) -> Compose a Identity a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (a (Identity a) -> Compose a Identity a)
-> (a a -> a (Identity a)) -> a a -> Compose a Identity a
forall b c a. (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 ~> Identity a) -> a a ~> a (Identity a)
forall a b. (a ~> b) -> a a ~> a b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> Identity a
a -> Identity a
forall a. a -> Identity a
Identity)
  associator :: forall (a :: Type -> Type) (b :: Type -> Type) (c :: Type -> Type).
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator Nat{} Nat{} Nat{} = (Compose (Compose a b) c .~> Compose a (Compose b c))
-> Nat (Compose (Compose a b) c) (Compose a (Compose b c))
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (a (Compose b c a) -> Compose a (Compose b c) a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (a (Compose b c a) -> Compose a (Compose b c) a)
-> (Compose (Compose a b) c a -> a (Compose b c a))
-> Compose (Compose a b) c a
-> Compose a (Compose b c) a
forall b c a. (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
. (b (c a) ~> Compose b c a) -> a (b (c a)) ~> a (Compose b c a)
forall a b. (a ~> b) -> a a ~> a b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map b (c a) ~> Compose b c a
b (c a) -> Compose b c a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (a (b (c a)) -> a (Compose b c a))
-> (Compose (Compose a b) c a -> a (b (c a)))
-> Compose (Compose a b) c a
-> a (Compose b c a)
forall b c a. (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
. Compose a b (c a) -> a (b (c a))
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose a b (c a) -> a (b (c a)))
-> (Compose (Compose a b) c a -> Compose a b (c a))
-> Compose (Compose a b) c a
-> a (b (c a))
forall b c a. (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
. Compose (Compose a b) c a -> Compose a b (c a)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)
  associatorInv :: forall (a :: Type -> Type) (b :: Type -> Type) (c :: Type -> Type).
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv Nat{} Nat{} Nat{} = (Compose a (Compose b c) .~> Compose (Compose a b) c)
-> Nat (Compose a (Compose b c)) (Compose (Compose a b) c)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (Compose a b (c a) -> Compose (Compose a b) c a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Compose a b (c a) -> Compose (Compose a b) c a)
-> (Compose a (Compose b c) a -> Compose a b (c a))
-> Compose a (Compose b c) a
-> Compose (Compose a b) c a
forall b c a. (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 (b (c a)) -> Compose a b (c a)
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (a (b (c a)) -> Compose a b (c a))
-> (Compose a (Compose b c) a -> a (b (c a)))
-> Compose a (Compose b c) a
-> Compose a b (c a)
forall b c a. (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
. (Compose b c a ~> b (c a)) -> a (Compose b c a) ~> a (b (c a))
forall a b. (a ~> b) -> a a ~> a b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map Compose b c a ~> b (c a)
Compose b c a -> b (c a)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (a (Compose b c a) -> a (b (c a)))
-> (Compose a (Compose b c) a -> a (Compose b c a))
-> Compose a (Compose b c) a
-> a (b (c a))
forall b c a. (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
. Compose a (Compose b c) a -> a (Compose b c a)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose)

instance MonoidalProfunctor (Nat :: CAT (Type -> Type)) where
  lift0 :: Nat Unit Unit
lift0 = Nat Identity Identity
Nat Unit Unit
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: Type -> Type). Ob a => Nat a a
id
  lift2 :: forall (x1 :: Type -> Type) (x2 :: Type -> Type)
       (y1 :: Type -> Type) (y2 :: Type -> Type).
Nat x1 x2 -> Nat y1 y2 -> Nat (x1 ** y1) (x2 ** y2)
lift2 = (x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
Nat x1 x2 -> Nat y1 y2 -> Nat (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 :: Type -> Type) (b :: Type -> Type) (c :: Type -> Type)
       (d :: Type -> Type).
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
par


instance CategoryOf (k1 -> k2 -> k3 -> Type) where
  type instance (~>) = Nat
  type Ob f = Functor f

instance Promonad (Nat :: CAT (k1 -> k2 -> k3 -> Type)) where
  id :: forall (a :: k1 -> k2 -> k3 -> Type). Ob a => Nat a a
id = Nat a a
forall {j} {k} (f :: j -> k). Functor f => Nat f f
n where
    n :: forall f. Functor f => Nat f f
    n :: forall {j} {k} (f :: j -> k). Functor f => Nat f f
n = (f .~> f) -> Nat f f
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (f :: j -> k) (a :: j) (b :: j).
Functor f =>
(a ~> b) -> f a ~> f b
map @f a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Nat b .~> c
f . :: forall (b :: k1 -> k2 -> k3 -> Type) (c :: k1 -> k2 -> k3 -> Type)
       (a :: k1 -> k2 -> k3 -> Type).
Nat b c -> Nat a b -> Nat a c
. Nat a .~> b
g = (a .~> c) -> Nat a c
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (b a ~> c a
b .~> c
f (b a ~> c a) -> (a a ~> b a) -> a a ~> c a
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k2 -> k3 -> Type) (c :: k2 -> k3 -> Type)
       (a :: k2 -> k3 -> Type).
(b ~> c) -> (a ~> b) -> a ~> c
. a a ~> b a
a .~> b
g)

instance Profunctor (Nat :: CAT (k1 -> k2 -> k3 -> Type)) where
  dimap :: forall (c :: k1 -> k2 -> k3 -> Type) (a :: k1 -> k2 -> k3 -> Type)
       (b :: k1 -> k2 -> k3 -> Type) (d :: k1 -> k2 -> k3 -> Type).
(c ~> a) -> (b ~> d) -> Nat a b -> Nat c d
dimap c ~> a
f b ~> d
g Nat a b
h = b ~> d
Nat b d
g Nat b d -> Nat c b -> Nat c d
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k1 -> k2 -> k3 -> Type) (c :: k1 -> k2 -> k3 -> Type)
       (a :: k1 -> k2 -> k3 -> Type).
Nat b c -> Nat a b -> Nat a c
. Nat a b
h Nat a b -> Nat c a -> Nat c b
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k1 -> k2 -> k3 -> Type) (c :: k1 -> k2 -> k3 -> Type)
       (a :: k1 -> k2 -> k3 -> Type).
Nat b c -> Nat a b -> Nat a c
. c ~> a
Nat c a
f
  (Ob a, Ob b) => r
r \\ :: forall (a :: k1 -> k2 -> k3 -> Type) (b :: k1 -> k2 -> k3 -> Type)
       r.
((Ob a, Ob b) => r) -> Nat a b -> r
\\ Nat{} = r
(Ob a, Ob b) => r
r


instance CategoryOf (k1 -> k2 -> k3 -> k4 -> Type) where
  type instance (~>) = Nat
  type Ob f = Functor f

instance Promonad (Nat :: CAT (k1 -> k2 -> k3 -> k4 -> Type)) where
  id :: forall (a :: k1 -> k2 -> k3 -> k4 -> Type). Ob a => Nat a a
id = Nat a a
forall {j} {k} (f :: j -> k). Functor f => Nat f f
n where
    n :: forall f. Functor f => Nat f f
    n :: forall {j} {k} (f :: j -> k). Functor f => Nat f f
n = (f .~> f) -> Nat f f
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (f :: j -> k) (a :: j) (b :: j).
Functor f =>
(a ~> b) -> f a ~> f b
map @f a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Nat b .~> c
f . :: forall (b :: k1 -> k2 -> k3 -> k4 -> Type)
       (c :: k1 -> k2 -> k3 -> k4 -> Type)
       (a :: k1 -> k2 -> k3 -> k4 -> Type).
Nat b c -> Nat a b -> Nat a c
. Nat a .~> b
g = (a .~> c) -> Nat a c
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (b a ~> c a
Nat (b a) (c a)
b .~> c
f Nat (b a) (c a) -> Nat (a a) (b a) -> Nat (a a) (c a)
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k2 -> k3 -> k4 -> Type) (c :: k2 -> k3 -> k4 -> Type)
       (a :: k2 -> k3 -> k4 -> Type).
Nat b c -> Nat a b -> Nat a c
. a a ~> b a
Nat (a a) (b a)
a .~> b
g)

instance Profunctor (Nat :: CAT (k1 -> k2 -> k3 -> k4 -> Type)) where
  dimap :: forall (c :: k1 -> k2 -> k3 -> k4 -> Type)
       (a :: k1 -> k2 -> k3 -> k4 -> Type)
       (b :: k1 -> k2 -> k3 -> k4 -> Type)
       (d :: k1 -> k2 -> k3 -> k4 -> Type).
(c ~> a) -> (b ~> d) -> Nat a b -> Nat c d
dimap c ~> a
f b ~> d
g Nat a b
h = b ~> d
Nat b d
g Nat b d -> Nat c b -> Nat c d
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k1 -> k2 -> k3 -> k4 -> Type)
       (c :: k1 -> k2 -> k3 -> k4 -> Type)
       (a :: k1 -> k2 -> k3 -> k4 -> Type).
Nat b c -> Nat a b -> Nat a c
. Nat a b
h Nat a b -> Nat c a -> Nat c b
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: k1 -> k2 -> k3 -> k4 -> Type)
       (c :: k1 -> k2 -> k3 -> k4 -> Type)
       (a :: k1 -> k2 -> k3 -> k4 -> Type).
Nat b c -> Nat a b -> Nat a c
. c ~> a
Nat c a
f
  (Ob a, Ob b) => r
r \\ :: forall (a :: k1 -> k2 -> k3 -> k4 -> Type)
       (b :: k1 -> k2 -> k3 -> k4 -> Type) r.
((Ob a, Ob b) => r) -> Nat a b -> r
\\ Nat{} = r
(Ob a, Ob b) => r
r



newtype NatK j k = NT (j -> k)
type instance UN NT (NT f) = f

data Nat' f g where
  Nat' :: (Functor f, Functor g)
       => { forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
Nat' ('NT f) ('NT g) -> f .~> g
getNat' :: f .~> g }
       -> Nat' (NT f) (NT g)

instance CategoryOf (NatK j k) where
  type instance (~>) = Nat'
  type Ob f = (Is NT f, Functor (UN NT f))

instance Promonad (Nat' :: CAT (NatK j k)) where
  id :: forall (a :: NatK j k). Ob a => Nat' a a
id = Nat' a a
Nat' ('NT (UN 'NT a)) ('NT (UN 'NT a))
forall {j} {k} (f :: j -> k). Functor f => Nat' ('NT f) ('NT f)
n where
    n :: forall f. Functor f => Nat' (NT f) (NT f)
    n :: forall {j} {k} (f :: j -> k). Functor f => Nat' ('NT f) ('NT f)
n = (f .~> f) -> Nat' ('NT f) ('NT f)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat' ('NT f) ('NT g)
Nat' (forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (f :: j -> k) (a :: j) (b :: j).
Functor f =>
(a ~> b) -> f a ~> f b
map @f a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  Nat' f .~> g
f . :: forall (b :: NatK j k) (c :: NatK j k) (a :: NatK j k).
Nat' b c -> Nat' a b -> Nat' a c
. Nat' f .~> g
g = (f .~> g) -> Nat' ('NT f) ('NT g)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat' ('NT f) ('NT g)
Nat' (f a ~> g a
f .~> g
f (f a ~> g a) -> (f a ~> f a) -> f a ~> g a
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 ~> f a
f a ~> g a
f .~> g
g)

instance Profunctor (Nat' :: CAT (NatK j k)) where
  dimap :: forall (c :: NatK j k) (a :: NatK j k) (b :: NatK j k)
       (d :: NatK j k).
(c ~> a) -> (b ~> d) -> Nat' a b -> Nat' c d
dimap = (c ~> a) -> (b ~> d) -> Nat' a b -> Nat' c d
Nat' c a -> Nat' b d -> Nat' a b -> Nat' 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 :: NatK j k) (b :: NatK j k) r.
((Ob a, Ob b) => r) -> Nat' a b -> r
\\ Nat'{} = r
(Ob a, Ob b) => r
r