Definite description in homotopy type theory

Question

I asked this question there and I have been suggested to ask it here.

In a paper by David Corfield, we have an account of definite description in homotopy type theory. The author gives the following rule:

Then we can describe the rule of what we might call the introduction:
X : Type,(x,p) : isContr(X) ⊢ the(X,x,p) ≡ x : X ,
where we typically do not think about the dependency on p. One explanation for ignoring p from the point of view of HoTT is that there can only be one such element since isContr(X) is a mere proposition (Lemma 3.11.4 of the HoTT book). So now we see that contractibility makes sense of our application of ‘the’ to an apparent groupoid such as ‘the product of two types A and B’. One might think that there could be many ways to produce such a product, but the universal property defining what it means to be a product ensures that any candidate is uniquely isomorphic to any other.

What I don't understand is that the(X,x,p) depends on x, while when we say ‘the product of two types A and B’ we don't specify any product in particular. If I had to formalize a "the introduction" rule that allows to speak about ‘the product of two types A and B’, I would formalize it as follows:

X : Type,(x,p) : isContr(X) ⊢ the(X) : X

Here, the(X) does not depend on any element of X in particular, all what we know is that it is an element of X, which seems to me to mimic what happens when we say ‘the product of two types A and B’: ‘the product of two types A and B’ is an element of the contractible type of the type of products of A and B and we cannot prove that the(X) ≡ x for some particular product x. What does justify David Corfield's rule and why did he not consider the rule stated here instead?

Answer 1

When you write $X : \operatorname{Type}, (x,p) : \operatorname{isContr}(X) ⊢ \dots$, regardless of what you write in the "$\dots$", it will depend on $X$ and $(x, p)$. For informal reasoning, it might be alright to suppress the dependency on $(x, p)$ since, as quoted, $\operatorname{isContr}(X)$ is a proposition and thus has at most one element up to equality: any two $(x, p), (x', p') : \operatorname{isContr}(X)$ give rise to an equality $(x, p) = (x', p')$ and hence an equality $\operatorname{the}(X, x, p) = \operatorname{the}(X, x', p')$.

You certainly have to have an element of $\operatorname{isContr}(X)$, since otherwise there isn't a unique element of $X$ to begin with. So in that sense, $\operatorname{the}$ depends on $x$ and $p$ in an essential way.

Having $\operatorname{the}(X)$ rather than $\operatorname{the}(X, x, p)$ introduces a serious problem with type checking. When checking that $\operatorname{the}(X, x, p) : X$, one has to confirm that $X$ is a type and that $(x, p) : \operatorname{isContr}(X)$. If we want to check that $\operatorname{the}(X) : X$ instead, we have to check that $X$ is a type and we have to produce a proof $\operatorname{isContr}(X)$ without any hint of where to start. This problem will generally be undecidable. For instance, any proposition is contractible if and only if it's true.

Put another way, $\operatorname{the}(X)$ violates the principle of type theory that the syntax of a term should determine the proof tree that checks its type (up to equivalence). This property is called syntax-directness and helps with proving certain properties of type theories such as invertibility of rules and canonicity.