Construir una función a partir de una proposición truncada

Question

En el comentario siguiente Cor 3.9.2 en el libro HoTT dice que hay que construir una función a partir de $ ||A|| $ a $ B $ definimos un predicado $ Q:B\to\mathcal{U} $ tal que $ \Sigma_{x:B}Q(x) $ es una mera proposición. Entonces construimos un $ f:A\to\Sigma_{x:B}Q(x) $ , obtiene un $ g:||A||\to\Sigma_{x:B}Q(x) $ por el principio de recursión del truncamiento proposicional y finalmente lo proyecta a $ B $ . Pero, ¿cómo puede $ \Sigma_{x:B}Q(x) $ sea una mera proposición si $ B $ ¿no es así? Porque esto significa que todos los elementos en $ \Sigma_{x:B}Q(x) $ son iguales, lo que indica que su primera componente debe ser igual. ¿Se supone que debe considerarse como un "subtipo" de $ B $ ¿aquí? También cuál es la conexión aquí con Cor 3.9.2 ?

Los libros dicen que un ejemplo de este método es el Ejercicio 3.19:

Supongamos que $ P:\mathbb{N}\to\mathcal{U} $ es una familia adecidable de meras proposiciones. Demostrar que $$ \Vert\Sigma_{n:\mathbb{N}}P(n)\Vert\to\Sigma_{n:\mathbb{N}}P(n). $$

Mi intento está abajo: $ P $ es decidible significa que cada $ P(n)$ satisface LEM Por lo tanto, o bien $ P(n)\simeq\mathbf{1} $ o $ P(n)\simeq\mathbf{0} $ . En el caso simple de que $ P(0)\simeq\mathbf{1} $ , considere la familia de tipos $ \Sigma_{n:\mathbb{N}}(0=n)\times P(n) $ Supongo que esto sería contraible y en paticular mera proposición. Así que el mapa constante $ (n,p_{n})\mapsto(0,\mathsf{refl}_{0},p_{0}) $ factores a través de $ \Vert\Sigma_{n:\mathbb{N}}P(n)\Vert $ . ¿Estoy en lo cierto? Además, esto requiere un poco de $ P(n_{0})\simeq\mathsf{1} $ pero, por lo general, no podemos garantizarlo. ¿Qué tal el caso general? ¿Alguien podría ayudarme? Gracias de antemano.

Answer 1

Sólo porque todos los elementos de $\sum_{x:B} Q(x)$ son iguales no significa que todos los elementos de $B$ son iguales, porque puede que no haya forma de seleccionar para cada $x:B$ un elemento de $Q(x)$ para elevarlo a un elemento de $\sum_{x:B} Q(x)$ .

Es cierto que si existe una función $f:\prod_{x:B} Q(x)$ y $\sum_{x:B} Q(x)$ es una proposición, entonces también lo es $B$ ya que para cualquier $x,y:B$ tenemos $(x,f(x)):\sum_{x:B} Q(x)$ y $(y,f(y)):\sum_{x:B} Q(x)$ Por lo tanto $(x,f(x))=(y,f(y))$ y así $x=y$ . Esto no es más que otra forma de decir que las proposiciones son cerradas bajo retracciones, ya que dar $f$ está exhibiendo $B$ como un repliegue de $\sum_{x:B} Q(x)$ .

Como ejemplo sencillo de cómo puede fallar esto, arregle algunos $b:B$ y que $Q(x) :\equiv (b=x)$ . Entonces $\sum_{x:B} Q(x)$ es un espacio-trayectoria de base, por lo tanto, es contraíble y, en particular, es una proposición. Pero $B$ podría haber sido cualquier tipo de punta.

Estoy de acuerdo en que la conexión con el punto 3.9.2 no está inmediatamente clara. Creo que probablemente la idea era tomar $A$ y $P$ en el lema para ser $\Vert A \Vert$ y la familia constante en $\sum_{x:B} Q(x)$ respectivamente. Entonces la función deseada $\Vert A\Vert \to \sum_{x:B} Q(x)$ se puede obtener del lema observando que $\sum_{x:B} Q(x)$ es una proposición (por supuesto) y que nuestra función $A\to \sum_{x:B} Q(x)$ rinde $\Vert A \Vert \to \Vert \sum_{x:B} Q(x)\Vert$ .

Answer 2

Para el ejercicio 3.19, puede utilizar que si $P$ es válida para algún número, existe un número mínimo para el que $P$ sostiene. Esto se puede demostrar mediante un algoritmo que recorre hacia abajo desde el número dado. El siguiente tipo es una mera proposición debido a la unicidad del número más pequeño:

$$\Sigma_{n:\mathbb{N}}P(n)\times({\textstyle\prod}_{m} P(m)\to n\leq m)$$

Por lo tanto, puede eliminar en él de $\Vert\Sigma_{n:\mathbb{N}}P(n)\Vert$ y luego proyectar los dos primeros componentes.