{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Instance.Nat where

import Data.Functor.Compose (Compose (..))
import Data.Functor.Const (Const (..))
import Data.Functor.Identity (Identity (..))
import Data.Functor.Product (Product (..))
import Data.Functor.Sum (Sum (..))
import Data.Kind (Type)
import Data.Void (Void, absurd)

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault, (//))
import Proarrow.Functor (Functor (..), type (.~>))
import Proarrow.Monoid (Comonoid (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..), PROD (..), Prod (..))
import Proarrow.Object.Coexponential (Coclosed (..))
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))

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
unNat :: f .~> g}
    -> Nat f g

(!) :: Nat f g -> a ~> b -> f a ~> g b
Nat f .~> g
f ! :: forall {j} {k} (f :: j -> k) (g :: j -> k) (a :: j) (b :: j).
Nat f g -> (a ~> b) -> f a ~> g b
! a ~> b
ab = f b ~> g b
f .~> g
f (f b ~> g b) -> (f a ~> f b) -> f a ~> g 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 ~> b) -> f a ~> f b
forall (a :: j) (b :: j). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> b
ab ((Ob a, Ob b) => f a ~> g b) -> (a ~> b) -> f a ~> g b
forall (a :: j) (b :: j) 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
ab

instance CategoryOf (k1 -> Type) where
  type (~>) = 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 (CategoryOf k1) => HasTerminalObject (k1 -> Type) where
  type TerminalObject = Const ()
  terminate :: forall (a :: k1 -> Type). Ob a => a ~> TerminalObject
terminate = (a .~> Const ()) -> Nat a (Const ())
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \a a
_ -> () -> Const () a
forall {k} a (b :: k). a -> Const a b
Const ()

instance (CategoryOf k1) => HasInitialObject (k1 -> Type) where
  type InitialObject = Const Void
  initiate :: forall (a :: k1 -> Type). Ob a => InitialObject ~> a
initiate = (Const Void .~> a) -> Nat (Const Void) a
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \(Const Void
v) -> Void -> a a
forall a. Void -> a
absurd Void
v

instance (Functor f, Functor g) => Functor (Product f g) where
  map :: forall (a :: k1) (b :: k1).
(a ~> b) -> Product f g a ~> Product f g b
map a ~> b
f (Pair f a
x g a
y) = f b -> g b -> Product f g b
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
f a -> g a -> Product f g a
Pair ((a ~> b) -> f a ~> f b
forall (a :: k1) (b :: k1). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> b
f f a
x) ((a ~> b) -> g a ~> g b
forall (a :: k1) (b :: k1). (a ~> b) -> g a ~> g b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> b
f g a
y)

instance HasBinaryProducts (k1 -> Type) where
  type f && g = Product f g
  fst :: forall (a :: k1 -> Type) (b :: k1 -> Type).
(Ob a, Ob b) =>
(a && b) ~> a
fst = (Product a b .~> a) -> Nat (Product a b) a
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \(Pair a a
f b a
_) -> a a
f
  snd :: forall (a :: k1 -> Type) (b :: k1 -> Type).
(Ob a, Ob b) =>
(a && b) ~> b
snd = (Product a b .~> b) -> Nat (Product a b) b
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \(Pair a a
_ b a
g) -> b a
g
  Nat a .~> x
f &&& :: forall (a :: k1 -> Type) (x :: k1 -> Type) (y :: k1 -> Type).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Nat a .~> y
g = (a .~> Product x y) -> Nat a (Product x y)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \a a
a -> x a -> y a -> Product x y a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
f a -> g a -> Product f g a
Pair (a a ~> x a
a a -> x a
a .~> x
f a a
a) (a a ~> y a
a a -> y a
a .~> y
g a a
a)

instance (Functor f, Functor g) => Functor (Sum f g) where
  map :: forall (a :: k1) (b :: k1). (a ~> b) -> Sum f g a ~> Sum f g b
map a ~> b
f (InL f a
x) = f b -> Sum f g b
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
f a -> Sum f g a
InL ((a ~> b) -> f a ~> f b
forall (a :: k1) (b :: k1). (a ~> b) -> f a ~> f b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> b
f f a
x)
  map a ~> b
f (InR g a
y) = g b -> Sum f g b
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
g a -> Sum f g a
InR ((a ~> b) -> g a ~> g b
forall (a :: k1) (b :: k1). (a ~> b) -> g a ~> g b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> b
f g a
y)

instance HasBinaryCoproducts (k1 -> Type) where
  type f || g = Sum f g
  lft :: forall (a :: k1 -> Type) (b :: k1 -> Type).
(Ob a, Ob b) =>
a ~> (a || b)
lft = (a .~> Sum a b) -> Nat a (Sum a b)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat a a ~> Sum a b a
a a -> Sum a b a
a .~> Sum a b
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
f a -> Sum f g a
InL
  rgt :: forall (a :: k1 -> Type) (b :: k1 -> Type).
(Ob a, Ob b) =>
b ~> (a || b)
rgt = (b .~> Sum a b) -> Nat b (Sum a b)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat b a ~> Sum a b a
b a -> Sum a b a
b .~> Sum a b
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
g a -> Sum f g a
InR
  Nat x .~> a
f ||| :: forall (x :: k1 -> Type) (a :: k1 -> Type) (y :: k1 -> Type).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Nat y .~> a
g = (Sum x y .~> a) -> Nat (Sum x y) a
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \case
    InL x a
x -> x a ~> a a
x a -> a a
x .~> a
f x a
x
    InR y a
y -> y a ~> a a
y a -> a a
y .~> a
g y a
y

data (f :~>: g) a where
  Exp :: (Ob a) => (forall b. a ~> b -> f b -> g b) -> (f :~>: g) a

instance (Functor f, Functor g) => Functor (f :~>: g) where
  map :: forall (a :: k1) (b :: k1).
(a ~> b) -> (:~>:) f g a ~> (:~>:) f g b
map a ~> b
ab (Exp forall (b :: k1). (a ~> b) -> f b -> g b
k) = a ~> b
ab (a ~> b) -> ((Ob a, Ob b) => (:~>:) f g b) -> (:~>:) f g b
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (b :: k1). (b ~> b) -> f b -> g b) -> (:~>:) f g b
forall {k} (a :: k) (f :: k -> Type) (g :: k -> Type).
Ob a =>
(forall (b :: k). (a ~> b) -> f b -> g b) -> (:~>:) f g a
Exp \b ~> b
bc f b
fc -> (a ~> b) -> f b -> g b
forall (b :: k1). (a ~> b) -> f b -> g b
k (b ~> b
bc (b ~> b) -> (a ~> b) -> a ~> b
forall (b :: k1) (c :: k1) (a :: k1).
(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
ab) f b
fc

instance (CategoryOf k1) => Closed (PROD (k1 -> Type)) where
  type f ~~> g = PR (UN PR f :~>: UN PR g)
  curry' :: forall (a :: PROD (k1 -> Type)) (b :: PROD (k1 -> Type))
       (c :: PROD (k1 -> Type)).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' (Prod Nat{}) (Prod Nat{}) (Prod (Nat Product b1 b1 .~> b1
n)) = Nat b1 (b1 :~>: b1) -> Prod Nat ('PR b1) ('PR (b1 :~>: b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod ((b1 .~> (b1 :~>: b1)) -> Nat b1 (b1 :~>: b1)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \b1 a
f -> (forall (b :: k1). (a ~> b) -> b1 b -> b1 b) -> (:~>:) b1 b1 a
forall {k} (a :: k) (f :: k -> Type) (g :: k -> Type).
Ob a =>
(forall (b :: k). (a ~> b) -> f b -> g b) -> (:~>:) f g a
Exp \a ~> b
ab b1 b
g -> Product b1 b1 b ~> b1 b
Product b1 b1 b -> b1 b
Product b1 b1 .~> b1
n (b1 b -> b1 b -> Product b1 b1 b
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
f a -> g a -> Product f g a
Pair ((a ~> b) -> b1 a ~> b1 b
forall (a :: k1) (b :: k1). (a ~> b) -> b1 a ~> b1 b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a ~> b
ab b1 a
f) b1 b
g) ((Ob a, Ob b) => b1 b) -> (a ~> b) -> b1 b
forall (a :: k1) (b :: k1) 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
ab)
  uncurry' :: forall (b :: PROD (k1 -> Type)) (c :: PROD (k1 -> Type))
       (a :: PROD (k1 -> Type)).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' (Prod Nat{}) (Prod Nat{}) (Prod (Nat a1 .~> (b1 :~>: b1)
n)) = Nat (Product a1 b1) b1 -> Prod Nat ('PR (Product a1 b1)) ('PR b1)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod ((Product a1 b1 .~> b1) -> Nat (Product a1 b1) b1
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \(Pair a1 a
f b1 a
g) -> case a1 a ~> (:~>:) b1 b1 a
a1 a -> (:~>:) b1 b1 a
a1 .~> (b1 :~>: b1)
n a1 a
f of Exp forall (b :: k1). (a ~> b) -> b1 b -> b1 b
k -> (a ~> a) -> b1 a -> b1 a
forall (b :: k1). (a ~> b) -> b1 b -> b1 b
k a ~> a
forall (a :: k1). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id b1 a
g)
  Prod (Nat a1 .~> b1
m) ^^^ :: forall (b :: PROD (k1 -> Type)) (y :: PROD (k1 -> Type))
       (x :: PROD (k1 -> Type)) (a :: PROD (k1 -> Type)).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Prod (Nat a1 .~> b1
n) = Nat (b1 :~>: a1) (a1 :~>: b1)
-> Prod Nat ('PR (b1 :~>: a1)) ('PR (a1 :~>: b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (((b1 :~>: a1) .~> (a1 :~>: b1)) -> Nat (b1 :~>: a1) (a1 :~>: b1)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \(Exp forall (b :: k1). (a ~> b) -> b1 b -> a1 b
k) -> (forall (b :: k1). (a ~> b) -> a1 b -> b1 b) -> (:~>:) a1 b1 a
forall {k} (a :: k) (f :: k -> Type) (g :: k -> Type).
Ob a =>
(forall (b :: k). (a ~> b) -> f b -> g b) -> (:~>:) f g a
Exp \a ~> b
cd a1 b
h -> a1 b ~> b1 b
a1 b -> b1 b
a1 .~> b1
m ((a ~> b) -> b1 b -> a1 b
forall (b :: k1). (a ~> b) -> b1 b -> a1 b
k a ~> b
cd (a1 b ~> b1 b
a1 b -> b1 b
a1 .~> b1
n a1 b
h)) ((Ob a, Ob b) => b1 b) -> (a ~> b) -> b1 b
forall (a :: k1) (b :: k1) 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
cd)

instance MonoidalProfunctor (Nat :: CAT (Type -> Type)) where
  par0 :: Nat Unit Unit
par0 = 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
  Nat x1 .~> x2
n par :: forall (x1 :: Type -> Type) (x2 :: Type -> Type)
       (y1 :: Type -> Type) (y2 :: Type -> Type).
Nat x1 x2 -> Nat y1 y2 -> Nat (x1 ** y1) (x2 ** y2)
`par` Nat y1 .~> y2
m = (Compose x1 y1 .~> Compose x2 y2)
-> Nat (Compose x1 y1) (Compose x2 y2)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (\(Compose x1 (y1 a)
fg) -> x2 (y2 a) -> Compose x2 y2 a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (x1 (y2 a) ~> x2 (y2 a)
x1 (y2 a) -> x2 (y2 a)
x1 .~> x2
n ((y1 a ~> y2 a) -> x1 (y1 a) ~> x1 (y2 a)
forall a b. (a ~> b) -> x1 a ~> x1 b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map y1 a ~> y2 a
y1 .~> y2
m x1 (y1 a)
fg)))

instance Monoidal (Type -> Type) where
  type Unit = Identity
  type f ** g = Compose f g
  leftUnitor :: forall (a :: Type -> Type). Ob a => (Unit ** a) ~> a
leftUnitor = (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). Ob a => a ~> (Unit ** a)
leftUnitorInv = (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). Ob a => (a ** Unit) ~> a
rightUnitor = (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). Ob a => a ~> (a ** Unit)
rightUnitorInv = (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).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = (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).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (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 Strong ((Nat :: CAT (Type -> Type))) (->) where
  act :: forall (a :: Type -> Type) (b :: Type -> Type) x y.
Nat a b -> (x -> y) -> Act a x -> Act b y
act (Nat a .~> b
n) x -> y
f = a y ~> b y
a y -> b y
a .~> b
n (a y -> b y) -> (a x -> a y) -> a x -> b y
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
. (x ~> y) -> a x ~> a y
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 x ~> y
x -> y
f
instance MonoidalAction (Type -> Type) Type where
  type Act (p :: Type -> Type) (x :: Type) = p x
  unitor :: forall x. Ob x => Act Unit x ~> x
unitor = Act Unit x ~> x
Identity x -> x
forall a. Identity a -> a
runIdentity
  unitorInv :: forall x. Ob x => x ~> Act Unit x
unitorInv = x ~> Act Unit x
x -> Identity x
forall a. a -> Identity a
Identity
  multiplicator :: forall (a :: Type -> Type) (b :: Type -> Type) x.
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator = Act a (Act b x) ~> Act (a ** b) x
a (b x) -> Compose a b x
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose
  multiplicatorInv :: forall (a :: Type -> Type) (b :: Type -> Type) x.
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv = Act (a ** b) x ~> Act a (Act b x)
Compose a b x -> a (b x)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose

newtype HaskRan j h a = Ran {forall {k} (j :: k -> Type) (h :: k -> Type) a.
HaskRan j h a -> forall (b :: k). (a -> j b) -> h b
runRan :: forall b. (a -> j b) -> h b}
instance Functor (HaskRan j h) where
  map :: forall a b. (a ~> b) -> HaskRan j h a ~> HaskRan j h b
map a ~> b
f (Ran forall (b :: k). (a -> j b) -> h b
k) = (forall (b :: k). (b -> j b) -> h b) -> HaskRan j h b
forall {k} (j :: k -> Type) (h :: k -> Type) a.
(forall (b :: k). (a -> j b) -> h b) -> HaskRan j h a
Ran \b -> j b
j -> (a -> j b) -> h b
forall (b :: k). (a -> j b) -> h b
k (b -> j b
j (b -> j b) -> (a -> b) -> a -> j b
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
a -> b
f)
instance Closed (Type -> Type) where
  type j ~~> h = HaskRan j h
  curry' :: forall (a :: Type -> Type) (b :: Type -> Type) (c :: Type -> Type).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' Nat{} Nat{} (Nat Compose a b .~> c
n) = (a .~> HaskRan b c) -> Nat a (HaskRan b c)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \a a
fa -> (forall b. (a -> b b) -> c b) -> HaskRan b c a
forall {k} (j :: k -> Type) (h :: k -> Type) a.
(forall (b :: k). (a -> j b) -> h b) -> HaskRan j h a
Ran \a -> b b
ajb -> Compose a b b ~> c b
Compose a b b -> c b
Compose a b .~> c
n (a (b b) -> Compose a b b
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((a ~> b b) -> a a ~> a (b b)
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 ~> b b
a -> b b
ajb a a
fa))
  uncurry' :: forall (b :: Type -> Type) (c :: Type -> Type) (a :: Type -> Type).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' Nat{} Nat{} (Nat a .~> HaskRan b c
n) = (Compose a b .~> c) -> Nat (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 a)
fja) -> HaskRan b c (b a) -> forall b. (b a -> b b) -> c b
forall {k} (j :: k -> Type) (h :: k -> Type) a.
HaskRan j h a -> forall (b :: k). (a -> j b) -> h b
runRan (a (b a) ~> HaskRan b c (b a)
a (b a) -> HaskRan b c (b a)
a .~> HaskRan b c
n a (b a)
fja) b a -> b a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  ^^^ :: forall (b :: Type -> Type) (y :: Type -> Type) (x :: Type -> Type)
       (a :: Type -> Type).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(^^^) (Nat b .~> y
by) (Nat x .~> a
xa) = (HaskRan a b .~> HaskRan x y) -> Nat (HaskRan a b) (HaskRan x y)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \HaskRan a b a
h -> (forall b. (a -> x b) -> y b) -> HaskRan x y a
forall {k} (j :: k -> Type) (h :: k -> Type) a.
(forall (b :: k). (a -> j b) -> h b) -> HaskRan j h a
Ran \a -> x b
x -> b b ~> y b
b b -> y b
b .~> y
by (HaskRan a b a -> forall b. (a -> a b) -> b b
forall {k} (j :: k -> Type) (h :: k -> Type) a.
HaskRan j h a -> forall (b :: k). (a -> j b) -> h b
runRan HaskRan a b a
h (x b ~> a b
x b -> a b
x .~> a
xa (x b -> a b) -> (a -> x b) -> a -> a b
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 -> x b
x))

data HaskLan j f a where
  Lan :: (j b -> a) -> f b -> HaskLan j f a
instance Functor (HaskLan j f) where
  map :: forall a b. (a ~> b) -> HaskLan j f a ~> HaskLan j f b
map a ~> b
g (Lan j b -> a
k f b
f) = (j b -> b) -> f b -> HaskLan j f b
forall {k} (j :: k -> Type) (f :: k) a (f :: k -> Type).
(j f -> a) -> f f -> HaskLan j f a
Lan (a ~> b
a -> b
g (a -> b) -> (j b -> a) -> j b -> b
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
. j b -> a
k) f b
f
instance Coclosed (Type -> Type) where
  type f <~~ j = HaskLan j f
  coeval' :: forall (a :: Type -> Type) (b :: Type -> Type).
Obj a -> Obj b -> a ~> ((a <~~ b) ** b)
coeval' Nat{} Nat{} = (a .~> Compose (HaskLan b a) b) -> Nat a (Compose (HaskLan b a) b)
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat (HaskLan b a (b a) -> Compose (HaskLan b a) b a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (HaskLan b a (b a) -> Compose (HaskLan b a) b a)
-> (a a -> HaskLan b a (b a)) -> a a -> Compose (HaskLan b a) b 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 a -> b a) -> a a -> HaskLan b a (b a)
forall {k} (j :: k -> Type) (f :: k) a (f :: k -> Type).
(j f -> a) -> f f -> HaskLan j f a
Lan b a -> b a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  coevalUniv' :: forall (b :: Type -> Type) (c :: Type -> Type) (a :: Type -> Type).
Obj b -> Obj c -> (a ~> (c ** b)) -> (a <~~ b) ~> c
coevalUniv' Nat{} Nat{} (Nat a .~> Compose c b
n) = (HaskLan b a .~> c) -> Nat (HaskLan b a) c
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \(Lan b b -> a
k a b
f) -> (b b ~> a) -> c (b b) ~> c a
forall a b. (a ~> b) -> c a ~> c b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map b b ~> a
b b -> a
k (Compose c b b -> c (b b)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (a b ~> Compose c b b
a b -> Compose c b b
a .~> Compose c b
n a b
f))

data CatAsComonoid k a where
  CatAsComonoid :: forall {k} (c :: k) a. (Ob c) => (forall c'. c ~> c' -> a) -> CatAsComonoid k a
instance Functor (CatAsComonoid k) where
  map :: forall a b. (a ~> b) -> CatAsComonoid k a ~> CatAsComonoid k b
map a ~> b
f (CatAsComonoid forall (c' :: k). (c ~> c') -> a
k) = (forall (c' :: k). (c ~> c') -> b) -> CatAsComonoid k b
forall {k} (f :: k) a.
Ob f =>
(forall (c' :: k). (f ~> c') -> a) -> CatAsComonoid k a
CatAsComonoid (a ~> b
a -> b
f (a -> b) -> ((c ~> c') -> a) -> (c ~> c') -> b
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
. (c ~> c') -> a
forall (c' :: k). (c ~> c') -> a
k)

instance (CategoryOf k) => Comonoid (CatAsComonoid k) where
  counit :: CatAsComonoid k ~> Unit
counit = (CatAsComonoid k .~> Identity) -> Nat (CatAsComonoid k) Identity
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \(CatAsComonoid forall (c' :: k). (c ~> c') -> a
k) -> a -> Identity a
forall a. a -> Identity a
Identity ((c ~> c) -> a
forall (c' :: k). (c ~> c') -> a
k c ~> c
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  comult :: CatAsComonoid k ~> (CatAsComonoid k ** CatAsComonoid k)
comult = (CatAsComonoid k .~> Compose (CatAsComonoid k) (CatAsComonoid k))
-> Nat
     (CatAsComonoid k) (Compose (CatAsComonoid k) (CatAsComonoid k))
forall {k} {k1} (f :: k -> k1) (g :: k -> k1).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat \(CatAsComonoid @a forall (c' :: k). (c ~> c') -> a
k) ->
    CatAsComonoid k (CatAsComonoid k a)
-> Compose (CatAsComonoid k) (CatAsComonoid k) a
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose
      ( forall (f :: k) a.
Ob f =>
(forall (c' :: k). (f ~> c') -> a) -> CatAsComonoid k a
forall {k} (f :: k) a.
Ob f =>
(forall (c' :: k). (f ~> c') -> a) -> CatAsComonoid k a
CatAsComonoid @a
          \(c ~> c'
f :: a ~> b) ->
            c ~> c'
f (c ~> c')
-> ((Ob c, Ob c') => CatAsComonoid k a) -> CatAsComonoid k a
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall (f :: k) a.
Ob f =>
(forall (c' :: k). (f ~> c') -> a) -> CatAsComonoid k a
forall {k} (f :: k) a.
Ob f =>
(forall (c' :: k). (f ~> c') -> a) -> CatAsComonoid k a
CatAsComonoid @b
              \c' ~> c'
g -> (c ~> c') -> a
forall (c' :: k). (c ~> c') -> a
k (c' ~> c'
g (c' ~> c') -> (c ~> c') -> c ~> c'
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
. c ~> c'
f)
      )

data ComonoidAsCat (w :: Type -> Type) a b where
  ComonoidAsCat :: (w a -> b) -> ComonoidAsCat w a b

instance (Functor w) => Profunctor (ComonoidAsCat w) where
  dimap :: forall c a b d.
(c ~> a) -> (b ~> d) -> ComonoidAsCat w a b -> ComonoidAsCat w c d
dimap c ~> a
f b ~> d
g (ComonoidAsCat w a -> b
h) = (w c -> d) -> ComonoidAsCat w c d
forall (w :: Type -> Type) a b. (w a -> b) -> ComonoidAsCat w a b
ComonoidAsCat (b ~> d
b -> d
g (b -> d) -> (w c -> b) -> w c -> d
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
. w a -> b
h (w a -> b) -> (w c -> w a) -> w c -> b
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
. (c ~> a) -> w c ~> w a
forall a b. (a ~> b) -> w a ~> w b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map c ~> a
f)

instance (Comonoid w) => Promonad (ComonoidAsCat w) where
  id :: forall a. Ob a => ComonoidAsCat w a a
id = (w a -> a) -> ComonoidAsCat w a a
forall (w :: Type -> Type) a b. (w a -> b) -> ComonoidAsCat w a b
ComonoidAsCat (Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> (w a -> Identity a) -> w 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
. Nat w Identity -> w .~> Identity
forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g
unNat w ~> Unit
Nat w Identity
forall {k} (c :: k). Comonoid c => c ~> Unit
counit)
  ComonoidAsCat w b -> c
f . :: forall b c a.
ComonoidAsCat w b c -> ComonoidAsCat w a b -> ComonoidAsCat w a c
. ComonoidAsCat w a -> b
g = (w a -> c) -> ComonoidAsCat w a c
forall (w :: Type -> Type) a b. (w a -> b) -> ComonoidAsCat w a b
ComonoidAsCat (w b -> c
f (w b -> c) -> (w a -> w b) -> w a -> c
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
. (w a ~> b) -> w (w a) ~> w b
forall a b. (a ~> b) -> w a ~> w b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map w a ~> b
w a -> b
g (w (w a) -> w b) -> (w a -> w (w a)) -> w a -> w b
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 w w a -> w (w a)
forall {k1} {k2} (f :: k1 -> Type) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose w w a -> w (w a))
-> (w a -> Compose w w a) -> w a -> w (w 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
. Nat w (Compose w w) -> w .~> Compose w w
forall {k} {k1} (f :: k -> k1) (g :: k -> k1). Nat f g -> f .~> g
unNat w ~> (w ** w)
Nat w (Compose w w)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult)

instance CategoryOf (k1 -> k2 -> k3 -> Type) where
  type (~>) = 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
Prof (b a) (c a)
b .~> c
f Prof (b a) (c a) -> Prof (a a) (b a) -> Prof (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).
Prof b c -> Prof a b -> Prof a c
. a a ~> b a
Prof (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 (~>) = 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
unNat' :: f .~> g}
    -> Nat' (NT f) (NT g)

instance CategoryOf (NatK j k) where
  type (~>) = 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