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.
• CommentAuthorDavid_Corfield
• CommentTimeDec 19th 2021
• (edited Dec 19th 2021)

In the term elimination row of the table in section 2, it seems to be taking $x: X$ as a variable under the bar. It should be the application of $f$ to an element judged to be in $X$, no? As we have it in section 3.

• CommentRowNumber2.
• CommentAuthorvarkor
• CommentTimeDec 19th 2021

Yes – I’ve corrected the mistake.

• CommentRowNumber3.
• CommentAuthorvarkor
• CommentTimeJul 11th 2022

Amend stated relationship between function types and product types as special cases of dependent product types.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeFeb 3rd 2023
• (edited Feb 3rd 2023)