Data type that represents the proof that two functions are equivalent

Question

I was trying to make a data type that represents that fact that two functions are equivalent. What does the error mean?

Code:

record FEq (f1 : a -> b) (f2 : a -> b) where
    constructor MkFEq
    unFEq : (x : a) -> (f1 x = f2 x)

Error:

Type checking ./FEq.idr
FEq.idr:1:1-3:36:
  |
1 | record FEq (f1 : a -> b) (f2 : a -> b) where
  | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
When checking type of Main.FEq.unFEq:
When checking argument x to type constructor =:
        Type mismatch between
                free_a b a f1 f2 rec
        and
                a

gallais gallais · Accepted Answer · 2018-11-23T22:37:38

AFAIK you are not allowed to mention unbound parameters in a record. So you have to add a and b as parameters like so:

record FEq a b (f1 : a -> b) (f2 : a -> b) where
  constructor MkFEq
  unFEq : (x : a) -> (f1 x = f2 x)

Data type that represents the proof that two functions are equivalent

1 Answers