Timeline for Provable `fun-ext`and "rewriting under binders" in intensional MLTT
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 3, 2023 at 19:57 | vote | accept | Russoul | ||
| Sep 3, 2023 at 17:00 | comment | added | Andrej Bauer |
You should not call it 'J' (taken by Martin-Löf) or K (taken by Streicher). There are still some letters left in the alphabet. It was already a bit annoying that in my comment above I had to write "your J" and "ordinary J".
|
|
| Sep 3, 2023 at 10:46 | comment | added | Russoul |
BTW, seriously, what's wrong with calling J a J? Am I mixing up names? Or is it about type-theory community wanting to phase the name out and replace with something else? Or did you mean I shouldn't call the new J a J? :P
|
|
| Sep 3, 2023 at 10:41 | comment | added | Russoul | Even if there is nothing else interesting, the new construction feels more satisfying somehow, as it encompasses fun-ext without extra axioms? | |
| Sep 3, 2023 at 10:36 | comment | added | Russoul |
Indeed, I just tried it myself, I can prove a single-argument version of new J from old J & fun-ext. But for me it is still like chicken and egg situation. You can prove extensionality principle for every other standard type former via J but not fun-ext... I was thinking, maybe J was "wrong"... Maybe there is something else interesting about multi-level contexts other than making fun-ext admissible.
|
|
| Sep 3, 2023 at 10:22 | answer | added | András Kovács | timeline score: 2 | |
| Sep 3, 2023 at 10:17 | comment | added | Russoul | What should I call it? :) | |
| Sep 3, 2023 at 8:38 | comment | added | Andrej Bauer |
Hmm, isn't your idea more or less a multi-argument combination of ordinary J and ordinary funext? In the ordinary funext we have just one variable to abstract over, and in ordinary J the telescope Δ is empty, whereas you allow a whole telescope. I would expect that your version of J (pleae don't call it J) is admissible with respect to the ordinary J and the ordinary funext.
|
|
| Sep 3, 2023 at 2:45 | comment | added | Russoul | Hm, Can I tag him here? I don't think one can tag a user in a comment unless the user has participated in the discussion. | |
| Sep 2, 2023 at 22:38 | comment | added | Andrej Bauer | I vaguely remember that Mike Shulman at some point was asking & thinking about having such multi-level contexts. Is he listening? | |
| Sep 2, 2023 at 20:22 | comment | added | Russoul |
Of course there is a lot to it, but hopefully that conveys the idea. All that's new is that we replace dependence on type (x : A) with dependence on family (Δ ⊦ x : A)
|
|
| Sep 2, 2023 at 20:21 | comment | added | Russoul |
≡ stands for the identity type, like in Agda. Regarding δ: just like we use the notation x. t to stand for a family t in the background context extended by some x : ?, I have δ.t standing for a family t in the background context extended by a telescope δ : ?. In that particular case δ : Δ. A context is a snoc-list of families of types (where families can depend on preceding families). Families can be eliminated just like variables in normal MLTT, but now we need to provide an instance of the context the family depends on.
|
|
| Sep 2, 2023 at 17:39 | comment | added | Andrej Bauer |
You should explain what Γ (Δ ⊦ α : A) (Δ ⊦ β : a₀ ≡ α) ⊦ B type is supposed to mean. What is a context, precisely? What are the judgement forms? You're changing these notions in a fundamental way, so you should explain the changes.
|
|
| Sep 2, 2023 at 17:37 | comment | added | Andrej Bauer |
Does ≡ stand for the identity type or judgemental equality? What is δ?
|
|
| Sep 2, 2023 at 11:33 | history | edited | Russoul | CC BY-SA 4.0 |
added 231 characters in body
|
| Sep 2, 2023 at 11:14 | history | asked | Russoul | CC BY-SA 4.0 |