Desde $\textsf{Prop}$ a $\textsf{Type}$

Question

Dejemos que $P,\top:\textsf{Prop}$ (donde $\textsf{Prop}$ es el universo de las meras proposiciones), $A=\{P,\neg P\}:\textsf{Type}$ y $B$ es una función de identidad tal que $B(x)=x$ . Dadas las definiciones anteriores, $(\star)$ se sostiene trivialmente. $$P\rightarrow(\top\rightarrow\Sigma x:A.B(x))\tag{$ \N - La estrella $}$$ Por el axioma de distribución de $\rightarrow$ obtenemos lo siguiente: $$(P\rightarrow\top)\rightarrow(P\rightarrow\Sigma x:A.B(x)).\tag{$ |star $}$$ Pero esto me parece impar porque $P\rightarrow\top$ es una mera proposición por definición, pero $P\rightarrow\Sigma x:A.B(x)$ no es una mera proposición sino un tipo. Por lo tanto, muestra que a partir de una prueba de una mera proposición (que es irrelevante para la prueba), obtenemos una prueba de un tipo (que es relevante para la prueba). Esto parece impar pero es natural en $(\star\star)$ .

Mi pregunta es: ¿qué es una condición general para un tipo de prueba irrelevante (de $\textsf{Prop}$ ) para implicar un tipo relevante para la prueba como en $(\star\star)$ ? Gracias.

Answer 1

$\newcommand{\inj}{\mathsf{inj}}$ $\newcommand{\refl}{\mathsf{refl}}$ $\newcommand{\isProp}{\mathsf{isProp}}$ $\newcommand{\isContr}{\mathsf{isContr}}$

No sé exactamente cuál es el origen de la confusión, pero he aquí algunas cosas en las que hay que pensar.

1. $⊤ → A$ equivale a $A$ Así que su $(\star)$ ya es equivalente a $P → Σx:A.B(x)$

2. Su $(*)$ ya tiene dos proposiciones que implican $Σx:A.B(x)$ por lo que no parece descabellado que una proposición lo implique (sobre todo porque $⊤$ es bastante vacuo).

3. Algunas no proposiciones son fáciles de exhibir a partir de cualquier proposición. Por ejemplo, $λ x. 0$ tiene tipo $⊤ → ℕ$

4. $P$ en realidad implica que $T = Σx:A.B(x)$ es contraíble (y por tanto una proposición) por el siguiente argumento:

   • Presumí $A$ significa algo equivalente a $ΣX:\mathcal U. \Vert (P=X)+(¬P=X) \Vert$ y así $B$ es $π_1$
   • $T$ está habitada por $(P, \vert ι_1 \refl \vert, p)$ , donde $p$ es la premisa. Dejemos que $(X, t, x)$ ser algún otro testigo
   • $P = X$ es una proposición porque $P$ es, usando $(B → \isProp(B)) → \isProp(B)$ con $B := (P = X)$
   • Esto nos permite deducir que $P = X$ utilizando el testigo truncado, porque $p$ y $x$ juntos refutan $¬P = X$
   • $p$ está relacionado con $x$ por el camino de $P$ a $X$ porque $P$ y $X$ son proposiciones
   • Los dos testigos truncados están relacionados porque los tipos truncados son proposiciones
   • Así, $(X, t, x)$ es igual a nuestro centro de contracción

5. $¬P$ implica que $T$ es contraíble por un argumento muy similar

6. $T → \isContr(T)$ porque $T$ nos da un valor $x : X$ , $\isContr(T)$ es una proposición, y por casos en $(P=X)+(¬P=X)$ podemos obtener un valor de $P$ o un valor de $¬P$ utilizar 4 o 5

7. Así, $T$ es una proposición, porque $(T → \isContr(T)) → \isProp(T)$ . Aquí es una formalización cúbica de Agda.

Sin embargo, el hecho de que $Σx:A.B(x)$ es en realidad una proposición es incidental. Si la fuente de tu pregunta es la idea de que las proposiciones en la HoTT están de alguna manera restringidas para que puedan ser "borradas", como en otras teorías de tipo, deberías abandonar eso. Una característica clave de la HoTT es que "irrelevante para la prueba" no significa "irrelevante desde el punto de vista computacional". Las meras proposiciones son irrelevantes para la prueba en el sentido de que para dos pruebas cualesquiera $p, q$ cualquier construcción sobre $p$ puede traducirse sistemáticamente a una construcción equivalente en $q$ . Sin embargo, esto no no significa que $p$ y $q$ no tienen contenido computacional.

Un ejemplo de ello son los conjuntos finitos. Uno puede definir el tipo de conjuntos finitos como:

$$ΣX:\mathcal U. \Vert Σn:ℕ. \mathsf{Fin}(n) \simeq X \Vert$$

Es decir, es la colección de tipos que son meramente equivalentes a algún conjunto de un tamaño finito particular. Sin embargo, se puede demostrar que para un determinado $X$ , $n$ es único, y puede extraerse del truncamiento. No existe ningún mecanismo para deducir el tamaño $n$ de $X : \mathcal U$ , por lo que la conclusión es que el truncamiento lo llevaba (al menos, si se espera una explicación computacional). Sólo hay obligaciones para acceder a ella.

Sin embargo, no creo que haya necesariamente una descripción general de "cuándo una proposición puede implicar a una no-proposición". Las proposiciones no están separadas/distinguidas arbitrariamente en HoTT. Son sólo tipos con una determinada propiedad definida, y hay múltiples razones conceptuales por las que un tipo puede tener esa propiedad.