[Agda] A tutorial on inference in Agda

[Roman]

Hi folks,

I wrote a tutorial on how Agda infers things:
https://htmlpreview.github.io/?https://github.com/effectfully/inference-in-agda/blob/master/InferenceInAgda.html

It targets the users of Agda and does not cover highly advanced topics
like higher-order unification, but otherwise it should be pretty
comprehensive.

Any comments, suggestions, ideas, criticism etc would be appreciated.

Best regards.