On Thursday, 15 November 2018 11:05:42 UTC, Martín Hötzel Escardó wrote:
(P → 𝓤) ≃ M
We take M := Σ (X : 𝓤), is-equiv (κ X),
where the function κ X : X → (P → X) is defined by κ x p = x
I think something interesting is happening here. We have the "open" modality
P → (-), and the sub-universe M of modal types coincides with the modal
reflection P → 𝓤 of the universe 𝓤. In particular, this means that the
sub-universe of modal types is itself a modal type. Has this kind of thing been
observed before, for this modality and possibly the classes of modalities
already considered in the literature?
Martin