What are instances of a dependent pair type?

Question

Currently I am learning about dependent pair ($\Sigma$-)types, and I'm having some trouble understanding how an instance of a dependent type could be formed. I think I understand how the type of a dependent pair looks, but how do values of that type look like in practice?

From my understanding, given a type $\Sigma(x:\tau).\tau'$, the members are pairs where the first entry has type $\tau$ and the second one has type which may depend on the value $\tau'[x\mapsto\tau]$, which generalizes $\tau\times\tau'$. For example $$ x_1,x_2:\tau \\ \tau'(x_1):=\tau_1 \\ \tau'(x_2):=\tau_2 \\ $$ Then if we have some $y_1:\tau_1,y_2:\tau_2$ then $$ (y_1,y_2):\Sigma(x:\tau).\tau' $$ But this raises a problem: in a clean, unnotated environment, the type of $(y_1,y_2)$ would be infereed to be $\tau_1\times\tau_2$. This is a problem because I still want the pair to be used in a context where a dependent pair is needed.

This has me confused, because by introducing a pair we are fixing $\tau'$. Do I have a wrong idea about what dependent pairs are supposed to be? What other way would there be to introduce a dependent pair? Is an annotation required for this concept to work?

Answer 1

In general, if you don't make extra annotations, then from a term $(a,b)$ there would be no way to tell what type you would like it to be. For example, $(3, \mathsf{refl})$ could be a term for $\sum_{n : \mathbb N} n=3$ or $\sum_{n:\mathbb N} n = n$.

How does some of the proof assistants circumvent this problem? In Agda, Coq, Lean and many others, the true type of the constructor is (modulo differences in actual syntax): $$\mathsf{mkPair}:\prod_{A:\mathscr U}\prod_{B:A \to\mathscr U}\prod_{a : A}B(a) \to \sum_{x:A}B(x)$$ So to use this, you need to provide $\mathsf{mkPair}(\color{blue}{A,B},a, b)$, so it is unambiguous that this is of type $\sum_{a:A}B(a)$.

On the other hand, why don't you need to write all that clogged up stuff when you make a dependent pair? This is because most proof assistants have a functionality called implicit argument, which infers some information so that some of those arguments can be omitted. Of course, it cannot infer from $(3,\mathsf{refl})$ what type you meant, so you'd still need to annotate.

A more minimalist annotation can be used, if you are to define dependent pairs by hand (instead of doing it in a systematic way called inductive types). Simply annotating the $B$ would be enough. For instance, $(3,\mathsf{refl})_{x.x=3}$ says that $B$ should be $B(a) = (a=3)$.

If you would really insist that the syntax doesn't contain the annotation at all (not even implicit), then you face the problem of non-unique typing.