I think to show this is an embedding may imply the law of double negation. For any proposition Q, let P = {0 : Z | Q}. Let A be defined as for all p : P, A(p) = 0 : P, and let B be defined as for all p : P, B(p) = not not (0 : P). To show that Pi (p : P), A(p) = Pi (p : P), B(p), you can define the following isomorphism (?): for any f : Pi (p : P), A(p), define g : Pi (p : P), B(p) by picking p : P, then f(p) : A(p), so Q is true. Hence, not not Q is true, meaning it has an element, so g(p) is that element. We then can conclude A = B. By function extensionality, that's equivalent to for all p : P, A (p) = B (p), which gives Q = not not Q.

Jean

On Tuesday, November 13, 2018 at 3:32:22 PM UTC-5, 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=𝟙)?

Martin