Bicategory constraint issue

Bicat.idr

-- We define uncurried versions of Pair and Either to help with type-checking
data Tuple : (Type, Type) -> Type where 
  MkTuple : a -> b -> Tuple (a, b)

data Sum : (Type, Type) -> Type where 
  Left : a -> Sum (a, b)
  Right : b -> Sum (a, b)

-- These are bifunctor versions of projections/injections
data Fst : (Type, Type) -> Type where 
  L : a -> Fst (a, b) 

data Snd : (Type, Type) -> Type where 
  R : b -> Snd (a, b) 

-- Natural transformations between bifunctors for Product and Sum
fst : Tuple a -> Fst a
fst (MkTuple l _) = L l 

snd : Tuple a -> Snd a
snd (MkTuple _ r) = R r  

left : Fst a -> Sum a 
left (L v) = Left v 

right : Snd a -> Sum a 
right (R v) = Right v 

-- Diagonal functor
Diag : a -> (a, a)
Diag t = (t, t) 

--copy : a -> Diag a 
--copy a = (a, a)

copy : a -> Tuple (a, a) 
copy a = MkTuple a a

cocopy : Sum (a, a) -> a
cocopy (Left a) = a 
cocopy (Right a) = a 

-- Natural transformations over some category arr
Nt : {s, t : Type} -> {arr : t -> t -> Type} -> (s -> t) -> (s -> t) -> Type
Nt {s, t} f g = {a : s} -> arr (f a) (g a)

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

IdrF : (Type -> Type) -> (Type -> Type) -> Type
IdrF = Nt {arr=Idr}

data Kind = T | ProdK Kind Kind | F Kind | U | TyOp

data Func : Kind -> Kind -> Type where
  -- Natural numbers, values are a functor from the terminal category
  N : Func U T
  -- List
  List : Func T T
  -- Product bifunctor
  ProdF : Func (ProdK T T) T
  -- Sum bifunctor
  SumF : Func (ProdK T T) T
  -- Diagonal functor
  DiagF : Func T (ProdK T T)

  -- First, Second projections
  FstF : Func (ProdK T T) T
  SndF : Func (ProdK T T) T 

  -- Identity functor
  Id : Func a a
  -- Functor composition
  Comp : {a, b, c : Kind} -> Func a b -> Func b c -> Func a c 


-- Natural transformations are indexed by functors, and correspond to functions (Type -> Type) -> (Type -> Type)
data Nats : {k1, k2 : Kind} -> Func k1 k2 -> Func k1 k2 -> Type where 
  -- reverse : List a -> List a 
  Reverse : Nats List List 
  -- Monad over Lists
  Pure : Nats Id List
  Join : Nats (Comp List List) List
  -- fst : (a, b) -> a 
  FstN : Nats ProdF FstF
  -- snd : (a, b) -> b
  SndN : Nats ProdF SndF 
  -- left : a -> Either a b
  LeftN : Nats FstF SumF
  -- right : b -> Either a b
  RightN : Nats SndF SumF
  -- copy : a -> (a, a)
  Copy : Nats Id (Comp DiagF ProdF)
  -- cocopy : Either a a -> a 
  Cocopy : Nats (Comp DiagF SumF) Id

  Identity : {f : Func k1 k2} -> Nats f f
  -- Horizontal composition of natural transformations
  HComp : {f, g, h : Func k1 k2} -> Nats f g -> Nats g h -> Nats f h
  -- Vertical composition of natural transformations
  VComp : Nats f g -> Nats h i -> Nats (Comp f h) (Comp g i)


Op : Kind -> Kind 
Op T = TyOp
Op U = U
Op TyOp = T 
Op (ProdK c1 c2) = ProdK (Op c1) (Op c2)
Op (F t) = F (Op t)

-- Our base kind is interpreted as Type
evK : Kind -> Type 
evK T = Type
evK U = Type
evK TyOp = Type
evK (F t) = List (evK t)
evK (ProdK k1 k2) = (evK k1, evK k2)

-- Functors
evFun : {k1, k2 : Kind} -> Func k1 k2 -> evK k1 -> evK k2
evFun List = List 
evFun N = \t => Nat
evFun FstF = Fst
evFun SndF = Snd
evFun ProdF = Tuple
evFun SumF = Sum
evFun DiagF = Diag
evFun Id = id
evFun (Comp {a, b, c} f g) = (evFun g) . (evFun f)

evHom : (k1, k2 : Kind) -> (evK k1) -> (evK k2) -> Type 
evHom k1 k2 = ?homs --evK k1 -> evK k2  

evNatTy : {k1, k2 : Kind} -> {f, g : Func k1 k2} -> Nats f g -> (evK k2 -> evK k2 -> Type)
evNatTy Reverse = Idr
evNatTy FstN = Idr
evNatTy SndN = Idr
evNatTy LeftN = Idr 
evNatTy RightN = Idr 
evNatTy Copy = Idr
evNatTy Cocopy = Idr
evNatTy Pure = Idr
evNatTy Join = Idr
evNatTy {k2} Identity = evHom k2 k2 
evNatTy {k2} (HComp n1 n2) = evHom k2 k2
evNatTy {k2} (VComp n1 n2) = evHom k2 k2

evNat : (n : Nats f g) -> Nt {arr=evNatTy n} (evFun f) (evFun g)
evNat Reverse = Prelude.List.reverse
evNat FstN = fst
evNat SndN = snd
evNat LeftN = left
evNat RightN = right
evNat Copy = copy
evNat Cocopy = cocopy
evNat Pure = pure
evNat Join = join
evNat Identity = ?ids
evNat (HComp n1 n2) = ?hcomp --(evNat n2) . (evNat n1)
evNat (VComp n1 n2) = ?vcomp -- \x => ((mapNT (evalNT  n2)) (evalNT n1 $ x))