We've finally finished the Idris book. Go us! Now let's look at what we learned from a different point of view.
Edwin Brady's 2013 paper "Idris, a General Purpose Dependently Typed
Programming Language: Design and
Implementation" (https://pdfs.semanticscholar.org/1407/220ca09070233dca256433430d29e5321dc2.pdf) describes how the Idris we know and love (well, sort of) is compiled into a simpler language, TT. If you're interested in the theoretical properties of Idris, what you really want to look at is the properties of TT.
The paper is a bit out of date -- the section on tactics, for example, is no longer of interest -- but the bulk of it is probably still helpful to anyone who wants a better understanding of Idris, or who is interested in learning to build a dependently typed language on top of a well-understood core language.
Let's read the paper, then get together to discuss it, along with anything else that comes to mind.
So far we've talked about the structure *in* categories. What about structure *between* categories? Functors tell us how to get from one category to another, or, in the case of endofunctors, from a category to itself.
In a programming language, an endofunctor manifests as a type-level function (or, depending on the language, something that just looks like a function), which takes a type as an argument and returns a type. You are probably familiar with a number of useful endofunctors, even if you haven't been calling them that.
Let's read the chapter and do the exercises, then get together for our usual lively and occasionally on-topic discussion. We'll try to get properly underway around 6:15.