zanzix

%hide Neg 

-- Base types. Unit, Bool, Monoid
data Ty = Unit | B | M | Ten Ty Ty | Sum Ty Ty | Neg Ty 

Val : Ty -> Type 
Val Unit = Unit 
Val (Sum a b) = Either (Val a) (Val b) 
Val (Ten a b) = (Val a, Val b) 
Val B = Bool 

zanzix

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

zanzix

-- Left kan extension w.r.t the functor j
data Lan : (j: k -> Type) -> (f : k -> Type) -> Type -> Type where 
  MkLan : {j: k -> Type} -> {a:k} -> (j a -> b) -> f a -> Lan j f b

-- The free relative monad over j
data Freest : {k : Type} -> (k -> Type) -> (k -> Type) -> k -> Type where
  Var  : {j : k -> Type} -> j v -> Freest j f v
  Bind : {j : k -> Type} -> Lan j f (Freest j f v) -> Freest j f v

-- General Functor