@falsifian I'll give it a try. I wanted to define a category. So I defined a record, containing the field object, which is the type of the category's objets. Then a field morphism, which has type object -> object -> Type.

After that, I added a field compose, which build a morphism from two morphisms. It's type is thus compose : {a, b, c : object} -> morphism a b -> morphism b c -> morphism a c.

Follow

@mavaxavou I haven't used Idris 1 in a while. Anyway, not sure if I'm understanding what you're trying to do; LMK.