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