Zulip Chat Archive

Stream: general

Topic: motives and threshold concepts

Gihan Marasingha (Jun 11 2021 at 00:51):

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.

Last updated: Aug 03 2023 at 10:10 UTC