Timeline for Very dependent functions
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 17, 2022 at 15:32 | comment | added | James Deikun | That's indeed the most troubling part of these rules. I don't have a full proof or prototype, but considering the occurrences of $f$ have to be structurally decreasing applications, as long as there's a substitution algorithm for the external form this should work out. A really precise specification of this would have a special part of the context for 'conjectured' $f$ of this sort, and maybe even a special judgement form and a copy of the elimination rule therein. (I've also tried to find some kind of alternate rules that have logical harmony but this is still the best I've come up with.) | |
| Dec 15, 2022 at 18:27 | comment | added | Mike Shulman | I have trouble understanding how rules like this would work in practice, and how we can believe that they will be well-behaved. Generally I think of a typechecking algorithm as taking some surface syntax (unchecked term) as input and producing some internal values (checked term) as output. The types appearing in a context, and the type being checked against, are always internal values. But here, in {}-form, you are placing $\{f\mid \Delta \to B\}$ in the context before you've finished typechecking it, so you don't have an internal value to put there. The other rules are similar. | |
| Sep 21, 2022 at 11:55 | comment | added | James Deikun | @AndrejBauer Edited, thanks. | |
| Sep 21, 2022 at 11:51 | history | edited | James Deikun | CC BY-SA 4.0 |
Fixed problems spotted by Andrej Bauer ... thanks!
|
| Sep 21, 2022 at 8:50 | comment | added | Andrej Bauer | The conclusion of {}-form seems to have an extraneous "$f :$" in the conclusion, and something is wrong with the context in the conclusion of {}-intro. | |
| S Sep 19, 2022 at 22:49 | review | First answers | |||
| Sep 24, 2022 at 11:51 | |||||
| S Sep 19, 2022 at 22:49 | history | edited | James Deikun | CC BY-SA 4.0 |
Added extra type condition to {}-elim to make the assumption in {}-form safer
|
| Sep 19, 2022 at 17:46 | history | edited | James Deikun | CC BY-SA 4.0 |
added 1 character in body
|
| Sep 19, 2022 at 17:44 | history | edited | James Deikun | CC BY-SA 4.0 |
added 27 characters in body
|
| Sep 19, 2022 at 17:40 | history | edited | James Deikun | CC BY-SA 4.0 |
added 4 characters in body
|
| Sep 19, 2022 at 17:39 | history | edited | James Deikun | CC BY-SA 4.0 |
edited body
|
| S Sep 19, 2022 at 17:36 | review | First answers | |||
| Sep 19, 2022 at 22:33 | |||||
| S Sep 19, 2022 at 17:36 | history | answered | James Deikun | CC BY-SA 4.0 |