Ejercicio 4.6 (iii) en el Libro HoTT

Question

Ser incapaz de resolver el Ejercicio 4.6 (iii) en la HoTT Libro, yo estaría muy agradecido por cualquier ayuda.

Recordar la declaración del Ejercicio 4.6:

Para $A,B:\mathcal U$, definir $$ \mathsf{idtoqinv}_{A,B}:(A=B)\a\sum_{f:A\to B}\mathsf{qinv}(f) $$ por el camino de la inducción de la manera obvia. Vamos $\mathsf{qinv}$-$\mathsf{univalence}$ indicar la forma modificada de la univalence axioma que afirma que para todos los $A,B:\mathcal U$ la función de $\mathsf{idtoqinv}_{A,B}$ tiene un cuasi-inversa.

(i) demuestre que $\mathsf{qinv}$-$\mathsf{univalence}$ puede ser utilizado en lugar de univalence en la prueba de la función extensionality en $\S$4.9.

(ii) demuestre que $\mathsf{qinv}$-$\mathsf{univalence}$ puede ser utilizado en lugar de univalence en la prueba del Teorema 4.1.3.

(iii) Demostrar que $\mathsf{qinv}$-$\mathsf{univalence}$ es inconsistente (es decir, permite la construcción de un habitante de 0). Por lo tanto, el uso de una "buena" de la versión de $\mathsf{isequiv}$ es esencial en la declaración de univalence.

Answer 1

Creo que usted tiene que demostrar que $\mathsf{qinv}(f)$ es una mera proposición para todos los $f$. Esto claramente contradice el Teorema 4.1.3 que resultó en (ii).

Esta respuesta es incorrecta, hay un problema señalado por Pierre-Yves Gaillard, ver su respuesta para una correcta.

Permite reescribir $\sum_{f:A\to B} \mathsf{qinv}(f)$$A \backsimeq B$, por lo que no hay que confundirlo con el "correcto" definición de equivalencia.

Para probar esto vamos a usar el Lema 4.1.1. Usted notará que la prueba de este lema utiliza el (normal) univalence axioma, pero esto no es un problema. Si usted mira más cerca, en la prueba de uno de los primeros usos de la lógica de la equivalencia de $\mathsf{isequiv}$$\mathsf{qinv}$, y sólo entonces, se aplica $\mathsf{ua}$. En nuestro caso, simplemente no hacer el primer paso, como el nuestro (incorrecto) versión de univalence nos da el deseado de equivalencia. Escribimos formalmente el tipo de el lema:

$$\mathsf{lemma} : \prod_{A,B:U} \prod_{f:A\to B} \mathsf{qinv}(f)\to(\mathsf{qinv}(f)\simeq\prod_{a:A}(a=a))$$

La hipótesis del lema es exactamente eso $f$ es una equivalencia en el sentido incorrecto. Así que el lema es equivalente a:

$$\mathsf{lemma'} : \prod_{A,B:U} \prod_{i:A\backsimeq B} (\mathsf{qinv}(\pi_1(i))\simeq\prod_{a:A}(a=a))$$

Ahora, lo que queremos demostrar es: $$\prod_{A,B:U} \prod_{i:A\backsimeq B} \prod_{a:A}\pi_1(\mathsf{lemma'}_{A,B}(i))(\pi_2(i))(a) = \mathsf{refl}_a$$ Porque esto muestra que, si $\mathsf{qinv}(f)$ está habitada, cada habitante es igual, en virtud de la equivalencia dada por el lema, a la función de $(\lambda a.\mathsf{refl}_a)$. Y así, el tipo es una mera proposición.

Tenga en cuenta que estamos utilizando la función extensionality, ya que sólo demostrar la la igualdad mediante la evaluación en cada $a:A$. También estamos utilizando la función extensionality en la prueba del lema. Así que el punto i) es necesario.

La última meta es fácil de probar. Por $\mathsf{\text{qinv-univalence}}$ podemos suponer que $i$ proviene de un camino en $A=B$. Y luego, por el camino de la inducción, podemos suponer que la ruta de acceso es la reflexividad. Entonces asumimos que: $$i \equiv \mathsf{idtoqinv}_{X,X}(\mathsf{refl}_X)$$

En este punto, sólo tiene que utilizar las definiciones de $\mathsf{lemma'}$, $\mathsf{lemma}$ en el caso trivial.

Este es básicamente el mismo argumento en el: https://groups.google.com/forum/#!msg/homotopytypetheory/EXWVbQNRAdE/ct89FgY1kVUJ

Answer 2

Como observa Luis, basta para demostrar que, para cualquier mapa de $f:A\to B$, el tipo de $\mathsf{qinv}(f)$ es una mera proposición.

Para cualquier tipos de $A$ $B$ ponemos $$ (A\simeq B):\equiv\sum_{f:A\to B}\mathsf{ishae}(f),\quad(A\backsimeq B):\equiv\sum_{f:A\to B}\mathsf{qinv}(f). $$ (Recordemos que $\mathsf{ishae}(f)$ es sinónimo de "$f$ es una media-adjoint de equivalencia".) Por el Teorema 4.2.3 y el comentario anterior, hay que dependen de las funciones $$ i:\prod_{A,B:\mathcal U}\prod_{f:A\to B}\mathsf{ishae}(f)\a\mathsf{qinv}(f),\quad p:\prod_{A,B:\mathcal U}\prod_{f:A\to B}\mathsf{qinv}(f)\a\mathsf{ishae}(f). $$ Para todos los $A,B:\mathcal U$ deje $e(A,B):(A=B)\to(A\backsimeq B)$ ser el natural de mapa (el que se supone admitir un cuasi-inversa).

Reclamo: si $f:A\to B$$x:\mathsf{qinv}(f)$,$i(A,B,f,p(A,B,f,x))=x$.

Desde $(f,x):A\backsimeq B$, podemos asumir por $\mathsf{qinv}$-univalence y la ruta de acceso de la inducción que $$ B\equiv Un,\quad f\equiv\mathsf{id}_A,\quad x\equiv e(a,a,\mathsf{refl}_A), $$ y la demanda sigue fácilmente de la definición de $i,p$$e$.

Para $f:A\to B$ $x,y:\mathsf{qinv}(f)$ tenemos $p(A,B,f,x)=p(A,B,f,y)$ porque $\mathsf{ishae}(f)$ es una mera proposición, y la afirmación implica $x=y$, según se requiera.