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

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.