Suma dependiente frente a los tipos de producto

Question

Sólo quiero aclarar la distinción y cómo los tipos de suma dependiente (sigma) generalizan los tipos de producto dependiente.

A menudo vemos que se utilizan vectores en los ejemplos. Así, por ejemplo, se introduce un tipo de producto con el mapeo de un número natural dado $n$ a un $n$ -tupla.

¿Es cierto que las sumas dependientes son más generales porque podríamos tener un mapeo de $n$ decir, un $m$ -tupla donde $n \neq m $ para cualquier $m, n$ ?

Gracias.

Answer 1

Las sumas dependientes, es decir, los tipos sigma, no generalizan los productos dependientes, es decir, los tipos pi. Tal vez quieras decir que generalizan pares lo cual es cierto simplemente a través de $\Sigma\ \_\!:\!A.B \cong A\times B$ . (Del mismo modo, $\Pi\ \_\!:\!A.B \cong A \to B$ .) De hecho, estos suelen ser los definiciones de $A\times B$ y $A\to B$ en las teorías de tipo dependiente.

$\mathsf{Vec}\ n\ A$ puede definirse como $\Pi n\!:\!\mathbb{N}.\mathsf{Fin}\ n\to A$ que, a través de una generalización directa del isomorfismo de curry, es isomorfo a $(\Sigma n\!:\!\mathbb{N}.\mathsf{Fin}\ n) \to A$ . Aquí $\mathsf{Fin}\ n$ es el tipo con exactamente $n$ valores. Se podría ver como $\mathsf{Fin}\ n \cong \{m\in\mathbb{N}\mid m < n\}$ . Con esta perspectiva $$\Sigma n\!:\!\mathbb{N}.\mathsf{Fin}\ n \cong \{(n,m)\in \mathbb{N}\times\mathbb{N}\mid m < n\}$$ De hecho, si $<$ es valorada por la proposición, lo que significa que $m < n$ está habitado por a lo sumo un valor, entonces los tipos de subconjuntos anteriores se pueden lanzar como sumas dependientes, por ejemplo $$\{(n,m)\in \mathbb{N}\times\mathbb{N}\mid m < n\} \cong \Sigma (n,m)\!:\!\mathbb{N}\times\mathbb{N}.m < n$$