Continuation modalities and Lawvere–Tierney topologies

[fredrik-bakke]

Defines continuation modalities as a generalization of the double negation modality, and shows they define Lavwere–Tierney topologies on types. It also improves term usage in the file about reflective subuniverses.

[fredrik-bakke]

With the addition of Lawvere–Tierney topologies, I wonder if this PR is relevant to #930.

[EgbertRijke]

Awesome pull request! Sorry that it took so long to get this PR reviewed, but the Lawvere-Tierney stuff is great!

I had some minor comments.

[fredrik-bakke]

Thanks for the review, and for catching the less-than-ideal phrasing!

After looking closer, I cannot find a good source for how to speak about the continuation monad either. If I understand correctly, it is the A → R in (A → R) → R that is the "continuation". The total expression should be read as "if we can compute R from A, then we can compute R", or "from a continuation on A we have a computation of R". And the act of using the continuation monad in programming can be referred to as "programming in continuation passing style".

In the context of the double negation modality, we should read it as "if A is empty, then we can deduce a contradiction." But, I am not an apprentice in the field of computability theory, and I don't know enough about the subject to give a satisfactory expository explanation. If I recall correctly, the reason I formalized continuations was mainly for the spurious connection I saw to the double negation modality.

I've reworded most of what I can find to refer to "the continuation monad" rather than "continuations". Let me know if this is satisfactory.

[EgbertRijke]

Thank you!