Defining categories in Idris

Question

I'm trying to define verified categories internal to Idris types, but my approach doesn't type check.

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 is the type of objects, mor a b is the type of morphisms from a to b. There are the right unit and associativity laws still to come, but already my definition for l doesn't work. It says:

 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)

I find that confusing. unit a has type mor a a, f has type mor a b, why doesn't comp (unit a) f have type mor a b as well?

Turion Turion · Accepted Answer · 2015-05-10T12:16:12

It only works if I explicitly give the implicit parameters:

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 {a=a} {b=a} {c=b} (unit a) f) = f

Edwin Brady points out in this issue, why. The reason is that there is no restriction on mor a b and mor b c being the actually same type. For example, mor could be a constant function. In that cases, the type checker can't infer a and b just from mor a b, which leads to the error message.

If one had the restriction that mor be an injective function (as will probably be done for class arguments in the future), it would be possible to infer a and b and no longer necessary to give the arguments implicitly.

Defining categories in Idris

1 Answers