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