Timeline for Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 21, 2022 at 17:57 | vote | accept | Max New | ||
| Jul 21, 2022 at 6:53 | history | edited | Jonathan Sterling | CC BY-SA 4.0 |
clean up
|
| Jul 21, 2022 at 6:48 | comment | added | Jonathan Sterling | @MaxNew added the example | |
| Jul 21, 2022 at 6:48 | history | edited | Jonathan Sterling | CC BY-SA 4.0 |
add explicit counterexample
|
| Jul 20, 2022 at 22:38 | comment | added | Max New | If you want to add in the explicit counterexample $$\forall k. \exists n. (\triangleright^k)^n \bot$$ we discussed on zulip I'll go ahead an accept the answer | |
| Jul 18, 2022 at 13:32 | comment | added | Max New | "Axiom of clockable choice"? | |
| Jul 18, 2022 at 12:46 | history | edited | Jonathan Sterling | CC BY-SA 4.0 |
My comments are no longer conjectural.
|
| Jul 18, 2022 at 12:19 | comment | added | Jonathan Sterling | Updated my answer accordingly. | |
| Jul 18, 2022 at 12:19 | history | edited | Jonathan Sterling | CC BY-SA 4.0 |
typo
|
| Jul 18, 2022 at 12:09 | comment | added | Jonathan Sterling |
That's right! Btw, I think that if A and \phi are both clock irrelevant, then it might in fact be possible to commute the existential under certain circumstances. Let me compute a bit more, and I'll update my answer.
|
|
| Jul 18, 2022 at 12:05 | comment | added | Max New | Oh I see, if you interpret the clock quantification as just a Pi type this is essentially a form of axiom of choice, and commuting with Sigma types is the usual “incorrect” rendering of AC. | |
| Jul 18, 2022 at 11:49 | comment | added | Jonathan Sterling | In fact, in MLTT for any type $K$ and families $k:K \vdash Ak$ and $k:K, x:Ak \vdash Bkx$ the sigma type commutation law that you described holds. | |
| Jul 18, 2022 at 11:31 | comment | added | Max New | Just to confirm: in these topos models the clock quantification does commute with Sigma types? | |
| Jul 18, 2022 at 10:41 | history | answered | Jonathan Sterling | CC BY-SA 4.0 |