Bicategory of Profunctors

ProfBicat.idr

-- Profunctor composition
data CompP : (k1 -> k2 -> Type) -> (k2 -> k3 -> Type) -> k1 -> k3 -> Type where 
InComp : {k1, k2, k3 : Type} -> {a : k1} -> {b : k2} -> {c : k3} -> {p : k1 -> k2 -> Type} -> {q : k2 -> k3 -> Type} 
  -> p a b -> q b c -> CompP p q a c 

-- Natural transformations over profunctors
Nt : {k1, k2 : Type} -> {arr : t -> t -> Type} -> (k1 -> k2 -> t) -> (k1 -> k2 -> t) -> Type  
Nt f g = {a : k1} -> {b : k2} -> arr (f a b) (g a b) 

-- Category of idris functions
Idr : Type -> Type -> Type
Idr a b = a -> b 

-- Vertical composition
pcomp : {p, q : k1 -> k2 -> Type} -> {r, s : k2 -> k3 -> Type} 
-> Nt {arr=Idr} p q -> Nt {arr=Idr} r s -> Nt {arr=Idr} (CompP p r) (CompP q s)
pcomp pq rs (InComp pab qbc) = InComp (pq pab) (rs qbc) 

-- one Kind for now
data Kind = T 

data Prof : Kind -> Kind -> Type where
-- HomT : (a -> b)
HomT : Prof T T
-- HomF : (f a -> f b)
HomF : Prof T T
-- HomM : (a -> f b)
HomM : Prof T T

-- Profunctor Identity
Id : {k1, k2 : Kind} -> Prof k1 k2 
-- Profunctor composition
Comp : {k1, k2, k3 : Kind} -> Prof k1 k2 -> Prof k2 k3 -> Prof k1 k3 

-- Natural transformations between profunctors
data Nats : {k1, k2 : Kind} -> Prof k1 k2 -> Prof k1 k2 -> Type where
-- id : (a -> b) -> (a -> b)
IdT : Nats HomT HomT
-- (.) : (b -> c) -> (a -> b) -> (a -> c)
Dot : Nats (Comp HomT HomT) HomT 
-- map : (a -> b) -> (f a -> f b)
Map : Nats HomT HomF
-- bind : (a -> m b) -> (f a -> f b)
Bind : Nats HomM HomF 
-- kl : (a -> b) -> (a -> f b)
Kl : Nats HomT HomM

-- arr : (a -> b) -> p a b
Arr : Nats Id HomM 
-- fish : (a -> m b) -> (b -> m c) -> (a -> m c)
Fish: Nats (Comp HomM HomM) HomM

-- Identity nat transform
NatId : {k1, k2 : Kind} -> {p : Prof k1 k2} -> Nats p p 
-- Horizontal composition
HComp : {k1, k2 : Kind} -> {f, g, h : Prof k1 k2} -> Nats f g -> Nats g h -> Nats f h
-- Vertical composition
VComp : {k1, k2, k3 : Kind} -> {p, q : Prof k1 k2} -> {r, s : Prof k2 k3} 
  -> Nats p q -> Nats r s -> Nats (Comp p r) (Comp q s)

-- Evaluate the kind
evK : Kind -> Type 
evK T = Type

-- Hom for functions between lists
homLs : Type -> Type -> Type
homLs a b = List a -> List b 

-- Hom for Kleisli (List)
homKl : Type -> Type -> Type 
homKl a b = a -> List b 

interface Profunctor (p : Type -> Type -> Type) where
promap : (a -> b) -> p b c -> (c -> d) -> p a d 

Profunctor Idr where 
promap l f r = \a => r (f (l a)) 

-- Evaluate profunctor
evProf : {k2 : Kind} -> Prof k1 k2 -> evK k1 -> evK k2 -> Type
evProf HomT = Idr
evProf HomF = homLs
evProf HomM = homKl
evProf (Id {k1=T, k2=T}) = Idr
evProf (Comp {k1=T, k2=T, k3=T} p q) = let 
ev1 = evProf p 
ev2 = evProf q in 
  \a => \b => CompP ev1 ev2 a b

-- Evaluate natural transformation between profunctors
evNat : (n : Nats {k1=k1} f g) -> Nt {arr=Idr} (evProf f) (evProf g)
evNat Map = map 
evNat IdT = id
evNat Bind = \f, ma => ma >>= f
evNat Kl = (.) pure
evNat Arr = (.) pure
evNat Fish = \(InComp f g) => f >=> g
evNat Dot = \(InComp f g) => g . f
evNat NatId = id
evNat (HComp n1 n2) = (evNat n2) . (evNat n1)
evNat (VComp {k1=T, k2=T, k3=T} n1 n2) = \x => pcomp (evNat n1) (evNat n2) x