-- | Work in Progress.
module Kindly.Rank2
  ( BFunctor,
    bmap,
    BFunctor2,
    bmap2,
  )
where

--------------------------------------------------------------------------------

import Kindly.Class

--------------------------------------------------------------------------------

type BFunctor b = FunctorOf ((->) ~> (->)) (->) b

bmap :: BFunctor b => forall f g. (forall x. f x -> g x) -> b f -> b g 
bmap :: forall (b :: (* -> *) -> *) (f :: * -> *) (g :: * -> *).
BFunctor b =>
(forall x. f x -> g x) -> b f -> b g
bmap forall x. f x -> g x
nat = Dom b f g -> Cod b (b f) (b g)
forall from to (f :: from -> to) (a :: from) (b :: from).
CategoricalFunctor f =>
Dom f a b -> Cod f (f a) (f b)
forall (a :: * -> *) (b :: * -> *). Dom b a b -> Cod b (b a) (b b)
map ((forall x. f x -> g x) -> Nat (->) (->) f g
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat f x -> g x
forall x. f x -> g x
nat)

type BFunctor2 b = FunctorOf ((->) ~> (->) ~> (->)) (->) b

bmap2 :: BFunctor2 b => forall f g. (forall x x'. f x x' -> g x x') -> b f -> b g 
bmap2 :: forall (b :: Cat (*) -> *) (f :: Cat (*)) (g :: Cat (*)).
BFunctor2 b =>
(forall x x'. f x x' -> g x x') -> b f -> b g
bmap2 forall x x'. f x x' -> g x x'
nat = Dom b f g -> Cod b (b f) (b g)
forall from to (f :: from -> to) (a :: from) (b :: from).
CategoricalFunctor f =>
Dom f a b -> Cod f (f a) (f b)
forall (a :: Cat (*)) (b :: Cat (*)).
Dom b a b -> Cod b (b a) (b b)
map ((forall x. (~>) (->) (->) (f x) (g x))
-> Nat (->) ((->) ~> (->)) f g
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat ((forall x. f x x -> g x x) -> Nat (->) (->) (f x) (g x)
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat f x x -> g x x
forall x. f x x -> g x x
forall x x'. f x x' -> g x x'
nat))