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=𝟙)?

Martin