Open mikeshulman opened 9 years ago
With no knowledge in category theory I have found it hard to understand intuitively the notion of recursion/induction:
As a conclusion, my experience is that the concept of free generation is a required step to fully understand the concept and the power of induction, for both standard and higher inductive types.
I think we did a fairly good job of not assuming too much background in topology and in type theory, but we did use a fair number of category-theoretic concepts without really explaining them in much detail. We could consider introducing these gradually, starting perhaps even in chapter 1 by describing how the recursion principles correspond to universal properties. @martinescardo has suggested that it could be helpful to also mention the universal property of Id earlier on.