Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I didn’t understand ’apd’. Is it a typo?
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.
Thanks!
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.
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.
1 to 6 of 6