On Tue, 13 Nov 2018, at 8:32 PM, Martín Hötzel Escardó wrote:
> Let P be a subsingleton and 𝓤 be a universe, and consider the
> product map
>
> Π : (P → 𝓤) → 𝓤
> A ↦ Π (p:P), A(p).
>
> Is this an embedding? (In the sense of having subsingleton
> fibers.)
>
> It is easy to see that this is the case if P=𝟘 or P=𝟙 (empty or
> singleton type).
>
> But the reasons are fundamentally different:
>
> (0) If P=𝟘, the domain of Π is equivalent to 𝟙, and Π amounts to
> the map 𝟙 → 𝓤 with constant value 𝟙.
>
> In general, a function 𝟙 → X into a type X is *not* an
> embedding. Such a function is an embedding iff it maps the
> point of 𝟙 to a point x:X such that the type x=x is a
> singleton.
>
> And indeed for X:=𝓤 we have that the type 𝟙=𝟙 is a singleton.
>
> (1) If P=𝟙, the domain of Π is equivalent to 𝓤, and Π amounts to
> the identity map 𝓤 → 𝓤, which, being an equivalence, is an
> embedding.
>
> Question. Is there a uniform proof that Π as above for P a
> subsingleton is an embedding, without considering the case
> distinction (P=𝟘)+(P=𝟙)?
I think one can show that ap Π is an equivalence by giving an inverse. Given X, Y : P → 𝓤, first note that the equality type X = Y is equivalent by function extensionality to (u : P) → X u = Y u. Since one can prove easily that (u : P) → X u = Π X, it follows that X = Y is equivalent to P → Π X = Π Y. Hence we get a map ω : Π X = Π Y → X = Y. To show that it is indeed an inverse of ap Π, start with some α : Π X = Π Y. By following the construction above, we get that ap Π (ω α) maps a function h : Π X to λ u . α (λ v . tr^X [u,v] (h u)) u, where [u,v] : u = v is given by the fact that P is a proposition. Now, within the assumption u : P, the λ expression in brackets is equal to h itself, hence ap Π (ω α) = α. The other composition is easier, since it can just be checked on reflexivity.
Best,
Paolo