dependent-type - Idris でのカテゴリーの定義

Question

Idris 型の内部で検証済みのカテゴリを定義しようとしていますが、私のアプローチでは型チェックが行われません。

class Cat ob (mor : ob -> ob -> Type) where 
  comp  : {a : ob} -> {b : ob} -> {c : ob} -> mor a b -> mor b c -> mor a c
  unit   : (a : ob) -> mor a a
  l     : {a,b : ob} -> {f : mor a b} -> (comp (unit a) f) = f

obはオブジェクトの型、は からまでmor a bの射の型です。適切な単位と結合法則はまだありますが、私の定義は既に機能していません。それは言います：abl

 When elaborating type of constructor of Main.Cat:
 When elaborating an application of comp:
         Can't unify
                 mor a13 b14 (Type of f)
         with
                 mor b14 c (Expected type)

私はそれが紛らわしいと思います。unit atypemor a aをf持っている、 type を持っているmor a b、どうしてcomp (unit a) ftypemor a bも持たないの?