Bicategories as 2d indexed algebras

Bicategory.idr

-- The Bicategory of endofunctors as a 2d indexed algebra

-- Natural transformations between functors (Type -> Type)
infixr 1 :~>
(:~>) : {o : Type} -> (o -> Type) -> (o -> Type) -> Type  
(:~>) f g = {a : o} -> f a -> g a 

-- | Syntax

-- 0-cells are Categories
data Cat = C 

-- 1-cells are Functors. We include identity, composition, and a generator for an endofunctor
data Func : Cat -> Type where 
  Endo : Func k
  I : Func k
  Comp : Func k -> Func k -> Func k

-- 2-cells are Natural Transformations. We include the generators for a monad. 
data NT : Func a -> Func b -> Type where
  Pure : NT a Endo
  Join : NT (Comp Endo Endo) Endo
  HComp : NT f g -> NT g h -> NT f h
  VComp : {g, f, h, i : Func a} -> NT g f -> NT h i -> NT (Comp g h) (Comp f i)

-- | Semantics

-- evaluate 0-cells to types
evalCat : Cat -> Type 
evalCat C = Type

-- evaluate 1-cells to endofunctors (Type -> Type). The 1-cell generator is evaluated to List. 
evalFun : {a : Cat} -> Func a -> (evalCat a -> evalCat a)
evalFun {a=C} Endo = List 
evalFun {a=C} I = id
evalFun {a=C} (Comp f1 f2) = (evalFun f1) . (evalFun f2)

-- evaluate 2-cells to natural transformations betwen functors (Type -> Type)
-- There's a constraint error here: "Can't solve constraint between: evalCat ?a and Type"
evalNT : NT f1 f2 -> ((evalFun f1) :~> (evalFun f2))
evalNT Pure = \x:a => pure x  
evalNT Join = \x => join x 
evalNT PureId = \i => pure (outId i)
evalNT (HComp n1 n2) = (evalNT n2) . (evalNT n1)
evalNT (VComp n1 n2) = \x => ((mapNT (evalNT n2)) (evalNT n1 $ x))