motives and threshold concepts

Stream: general

[Gihan Marasingha]

The latest exlean post is on the topics I struggled with in #tpil Chapter 7, viz. motives, minor and major premises. I've done my best to motivate the motive concept in the special case of eliminators on nat. I plan to do a follow-up post looking at other inductive types.

From a pedagogical perspective, I posit that having to treat a particular mathematical object as both having a type and being a type raises similar challenges to those faced by students needing to treat an object simultaneously as being a set and being an element of a set.