Explain more category theory

[mikeshulman]

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.

[louisGarde]

With no knowledge in category theory I have found it hard to understand intuitively the notion of recursion/induction:

• for N recursion/induction seems easy, but the fact that type theory only needs 3 axioms (2 constructors and 1 induction principle) where Peano needs 5 looks like an unexplained miracle !
• for higher inductive type (starting from equality) my intuition was getting lost, I was unable to make the link with the induction principle for N. Again, the power of the equality types looks like an unexplained miracle! I have solved these 2 difficulties after reading Steve Awodey's lectures on category theory, with the very nice explanation of the concept of free generation in chapter 1.7 using free monoid. I think that you should from the very beginning (chapter 1.5 with the first explanation of the "type introduction pattern") clarify the concept of free generation and explain that the induction principle is designed so that the type is freely generated by its constructors, with the "no noise" and "no junk" properties (as explained by Steve Awodey). The concept of free generation should be explained without Category theory; but I think this is possible, Steve Awodey's explanation using free monoid is already very near the goal.

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.