There isn’t much you can prove but when I was first learning about it in HoTT I found it a lot easier and intuitive to use circle recursion. I wouldn’t have gotten very far with induction without some more work. So perhaps I should of said: it’s easier to use circle recursion than induction. I’ll take back what I said about most things.
]]>For most things you will only ever use circle recursion which tells you how to build a function out of the circle.
I’m not sure what you mean by that. I can’t think offhand of much that you can prove about the circle using recursion but not induction.
]]>Thanks!
]]>apd is dependent ap
is the application of to
So instead of applying a function to both sides, we apply a dependent function (the result isn’t a path type anymore but a dependent path). See page ~92 in the HoTT book.
In this case this was written before I modified the page.
Edit:
For most things you will only ever use circle recursion which tells you how to build a function out of the circle. Circle induction tells you how to build a dependent function out the circle.
]]>I didn’t understand ’apd’. Is it a typo?
]]>cleaned up page and added a small ideas section too
]]>