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

$apd_f(p)$ is the application of $f : \prod_{(a:A)} B(a)$ to $p : x =_A y$

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

]]>