El axioma K de Streicher pero para la Lista

Question

Parte de la intuición detrás de la relajación del axioma K de Streicher ("el único habitante del tipo de identidad es la reflexividad") es: "sí, sólo hay un uniformemente definible elemento del tipo de identidad $\mathrm{Id}_A$ como $A$ varía en todos los tipos, pero ¿por qué debería significar eso que sólo hay un elemento de $\mathrm{Id}_{\mathrm{Bool}}$ ?".

$\mathrm{List}_A$ puede definirse mediante los dos constructores $\mathrm{Empty} : \mathrm{List}_A$ y $\mathrm{Cons} : A \to \mathrm{List}_A \to \mathrm{List}_A$ .

¿Hay algún axioma implícito aquí de que los únicos habitantes de $\mathrm{List}_A$ son los que se hacen a partir de esos dos constructores, es decir, una especie de K-pero-para-listas? Si relajáramos ese axioma, ¿qué podría ser un miembro "no uniformemente definible" de $\mathrm{List}_{\mathrm{Bool}}$ ¿se ve así? ¿O es que, de alguna manera, sólo $\mathrm{Id}$ tiene esta propiedad (lo que me parece un poco improbable)?

Reconozco que podríamos declarar arbitrariamente que $\mathrm{Fish}$ es miembro de $\mathrm{List}_{\mathrm{Bool}}$ pero eso parece extremadamente artificial (mucho más que "las identidades son las equivalencias" de la univalencia).

Answer 1

Lo que hace esto para $\mathsf{List}_A$ es el eliminador inductivo. Tenemos un eliminador inductivo que también nos permite demostrar fácilmente $\prod_{A:\mathcal U}\prod_{x:A}\mathsf{isContr}(\sum_{y:A}\mathsf{Id}_A(x,y))$ donde $\mathsf{isContr}(T)\equiv\prod_{x,y:T}(\mathsf{Id}_T(x,y))$ lo que significa $(x,\mathsf{refl}_x)$ es el valor "único" de $\sum_{y:A}\mathsf{Id}_A(x,y)$ para cualquier $A$ y $x$ .

La cuestión es que la definición de $\mathsf{Id}_A(x,y)$ es indexado (no parametrizado) en $y$ . Esto significa que la definición no dice que $\mathsf{Id}_A(x,y)$ se define inductivamente para cada $A$ , $x$ y $y$ pero que $\sum_{y:A}\mathsf{Id}_A(x,y)$ es para todos los casos apropiados $A$ y $x$ . (Podríamos indexar por $x$ que también lleva a $\sum_{x,y:A}\mathsf{Id}_A(x,y)$ que se define inductivamente, pero esto equivale a tener $x$ sea un parámetro). Por lo tanto, no tenemos ninguna base para suponer que $\mathsf{refl}_x$ es el único valor de tipo $\mathsf{Id}_A(x,x)$ porque no es un tipo definido inductivamente en general.

No hay nada terriblemente especial en $\mathsf{Id}$ . Algo similar puede aplicarse a cualquier tipo inductivo indexado. Por ejemplo, aquí está la pertenencia a una lista definida como una relación definida inductivamente en Agda:

data _∈_ {A : Set} : A → List A → Set where
    Here : {x : A} → {xs : List A} → x ∈ Cons x xs
    There : {x y : A} → {xs : List A} → x ∈ xs → x ∈ Cons y xs

Esto debería tener el mismo tipo de problemas que $\mathsf{Id}$ (lo cual no es sorprendente, ya que estoy bastante seguro de que puede demostrar que $\mathsf{Id}_A(x,y)$ equivale a $x\in_A\mathsf{Cons}(y,\mathsf{Empty})$ ). Es decir, afirmo que no se puede demostrar (sin $\mathsf K$ ) que $x\in_A\mathsf{Cons}(x,\mathsf{Empty})$ sólo está habitada por $\mathsf{Here}_{x,\mathsf{Empty}}$ .

Postulando $\mathsf{Fish}:\mathsf{List}_{\mathsf{Bool}}$ no crea un nuevo valor de $\mathsf{List}_{\mathsf{Bool}}$ . Sólo produce una nueva constante que es un valor de $\mathsf{List}_{\mathsf{Bool}}$ pero no sabemos cuál es ese valor. Todavía podemos hacer una inducción estructural sobre él o demostrar que no puede ser otra cosa que $\mathsf{Empty}$ o $\mathsf{Cons}(x,xs)$ para algún tipo de $x$ y $xs$ . Simplemente no podemos calcular con ella porque no sabemos cuál es.