Re: [HoTT] Re: Proof that something is an embedding without assuming excluded middle?

[Michael Shulman <shulman@sandiego.edu>]

I remember noticing before that the P x (-) co-modal types coincide
with the P -> (-) modal ones.  In topos-theoretic language, these
common sub-universes are the slice category E/P, which is related to E
by an essential geometric embedding, hence an adjoint triple i_! -|
i^* -| i_* in which both i_! and i_* are fully faithful.  The left
adjoint i_! embeds E/P as the P x (-) co-modal types, while the right
adjoint i_* embeds it as the P -> (-) modal ones.
On Thu, Nov 15, 2018 at 2:26 PM Martín Hötzel Escardó
<escardo.martin@gmail.com> wrote:
>
>
>
> 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.

-- 
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.