Timeline for Provable `fun-ext`and "rewriting under binders" in intensional MLTT
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 3, 2023 at 19:57 | vote | accept | Russoul | ||
| Sep 3, 2023 at 17:01 | comment | added | Andrej Bauer | @Russoul: Maybe. The burden on proof is on the person suggesting that there is such a thing. | |
| Sep 3, 2023 at 10:40 | comment | added | Russoul |
But maybe if we reformulate type theory via the "family of types" contexts instead of "plain types" contexts the new J would reflect some universal property?
|
|
| Sep 3, 2023 at 10:22 | history | answered | András Kovács | CC BY-SA 4.0 |