Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorAli Caglayan
• CommentTimeJan 19th 2019

cleaned up page and added a small ideas section too

• CommentRowNumber2.
• CommentAuthorTodd_Trimble
• CommentTimeJan 19th 2019

I didn’t understand ’apd’. Is it a typo?

• CommentRowNumber3.
• CommentAuthorAli Caglayan
• CommentTimeJan 19th 2019
• (edited Jan 19th 2019)

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.

• CommentRowNumber4.
• CommentAuthorTodd_Trimble
• CommentTimeJan 19th 2019

Thanks!

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeJan 19th 2019

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.

• CommentRowNumber6.
• CommentAuthorAli Caglayan
• CommentTimeJan 20th 2019

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.