Just to note, Edwin was the original author of Idris, so I'd definitely recommend watching his talk.

Edit:

Given that my comment seems fairly high at the moment, I'll post a link to his PhD thesis, which seems to be the genesis of Idris for anyone interested: http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf