On Thursday, 15 November 2018 19:30:08 UTC, Michael Shulman wrote:
>
> However, this sub-universe coinciding with the modal reflection of the 
> whole universe seems to be something very special about open 
> modalities. 
>

We may consider the dual question of whether Σ is an embedding:

 s : (P → 𝓤) → 𝓤
 s = Σ

This is again a section of the same retraction r : 𝓤 → (P → 𝓤) defined
by

 r X p = X.

This time we have that the idempotent s ∘ r satisfies

 s (r X) = P × X

definitionally.

So consider the projection κ : (X : 𝓤) → s (r X) → X
and the sub-universe determined by this co-modal operator P × (-):

 C := Σ \(X : 𝓤) → is-equiv (κ X)

Then again we have a definitional factorization of s as

 (P → 𝓤) ≃ C ↪ 𝓤,

where the embedding is the projection, showing that s = Σ is an
embedding too, and that M ≃ C, even though the fixed points of P → (-)
and P × (-) are quite different if e.g. P = 𝟘.

So the subuniverse of P × (-) - co-modal types coincides with the
P → (-) - modal reflection of the universe.

(I coded this in Agda to be sure this is not an evening mirage,
available at the same place. The proof was produced by copy and paste
of the previous one, with very few modifications.)

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.