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 : {k2 : Kind} -> {f : Func k1 k2} -> Nats f f
  -- Horizontal composition of natural transformations
  HComp : {k2 : Kind} -> {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 : 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)

evHomTy : (k : Kind) -> (evK k) -> (evK k) -> Type 
evHomTy T = Idr
evHomTy (ProdK x y) = \l, r => (evHomTy x (fst l) (fst r), evHomTy y (snd l) (snd r))
-- evHomTy (F x) = ?homs_2
evHomTy U = Idr
evHomTy TyOp = Idr

evHomComp :
  (k2 : Kind) ->
  {f, g, h : evK k1 -> evK k2} ->
  Nt {arr=evHomTy k2} f g ->
  Nt {arr=evHomTy k2} g h ->
  Nt {arr=evHomTy k2} f h
evHomComp k = ?something_something

evHomId : (k : Kind) -> {f : Func k1 k} -> Nt {arr=evHomTy k} (evFun f) (evFun f)
evHomId T = \x => x
evHomId (ProdK x y) = (?rec_on_the_left, ?rec_on_the_right)
evHomId U = \x => x
evHomId TyOp = \x => x

evNatTy : Nats {k2=k2} 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 (Identity {k2}) = evHomTy k2
evNatTy (HComp {k2} n1 n2) = evHomTy k2
-- evNatTy {k2} (VComp n1 n2) = evHomTy 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 {k2 = k}) = evHomId k
evNat (HComp {k2} n1 n2) = ?todo -- evHomComp k2 (evNat n1) (evNat n2)
-- evNat (VComp n1 n2) = ?vcomp -- \x => ((mapNT (evalNT  n2)) (evalNT n1 $ x))