{-# 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