Every mere proposition is a set?

Question

In the HoTT Book, lemma 3.3.4 states that "every mere proposition is a set", where a mere proposition is a type $A$ such that $IsProp(A) = \prod_{x,y: A}(x=_Ay)$ holds, and a set is a type $A$ such that $IsSet(A) = \prod_{x,y:A} IsProp(x=_Ay)$ holds.

The proof of this lemma starts with "Fix $x:A$ [insert proof].", but never discharges the $x:A$ (as far as I can see).

So in fact, what the proof does is exhibit an element of type $\prod_{x:A}( isProp(A)\to IsSet(A))$, in other words of type $A\to isProp(A)\to IsSet(A)$ : as far as I can see, this not enough to get an element of type $isProp(A) \to IsSet(A)$ (without excluded middle) : am I missing something ?

If not, how can one fix the proof ?

Answer 1

It does discharge $x$. The statement being proved is $\prod_{x, y: A} \prod_{p, q: x = y} p = q$ (i.e. $\text{IsSet} A$) under the assumption of $f: \text{IsProp} A$. Along the way, the statement $\prod_{y, z: A} \prod_{p: y = z} p = g(y)^{-1} \cdot g(z)$ is proved, but then it's instantiated with $y := x$ and $z := y$ for the last line.

Answer 2

We can think of a proposition multiple ways:

We can think of a proposition of a statement that is either true or false

An example of a statement:

Peter is eating

This whole statement is either true or false.

Next we can also see this as a proposition composed of one single statement without using any logical connectives.

For example

Let $Q$ denote the proposition for the statement "Peter is drinking" This single proposition can be seen as the truth table of possible combinations of $Q$ being a single proposition that is not a composition of other propositions.

Truth table of Q, with on the left the given input values and on the right the result of the proposition.

Next we can use these non composed propositions in combination with our logical connectives to build more complex statements. This can either be by connecting the $Q$ in different ways or by using other defined statements. For example

We compose the following statement "Peter is drinking and Peter is not drinking." to be the proposition.

$Q \land \neg(Q)$ We can also define it with another Letter to denote this statement.

Notice we still are using one "building block" proposition. That is how we defined Q. Yet by using the and connective and the negation we now have a whole different outcome for each combination we originally assign Q to be. This new statement will always be false regardless of the value of the non composed statement of $Q$

Thus we can conclude we have two different composed propositions:

Q as a proposition composed of one single proposition. $Q \land \neg(Q)$ as a proposition composed Q connected to negation of Q using the and connective to connect them $Q$ with $\neg(Q)$. And using $\neg$ to negate the $Q$

This will have the following truth table with possible inputs on the left column and the evaluation of all the possible outcomes of the proposition as whole:

To conclude: We have a non composed proposition which is a single statement which can either be True or False.

We have a composed proposition without connectives which can have different possible inputs for True or False, yet the result of the statement depends on the input True or false.

We have composed propositions which are multiple propositions that are chained together using logical connectives. For each distinct non composed proposition we have can have input True or False. The chaining of these values will eventualy result in either True or False for the proposition as a whole depending on the given input values.