Dos preguntas sobre homotopía tipo teoría

Question

En la lectura de la HoTT libro, he encontrado que es fácil quedar empantanado en detalle y duro para decirle a los generales "cuadro grande" de lo que está pasando. Espero obtener alguna respuesta general a las siguientes dos preguntas.

1. Sé que la declaración de la univalence axioma, que es, para los tipos de $A$ $B$ en algunos universo $\mathcal{U}$ $$ (A = B) \simeq (A \simeq B). $$ Esto es por lo general por escrito junto con una interpretación algo así como "Si a y B son equivalentes, como entonces, los tipos son iguales como los tipos", pero esto no parece del todo correcto - es cierto sólo hasta equivalencia. Por qué hacemos caso omiso de la equivalencia en el axioma, y tratar a los dos como si en realidad eran el mismo?

2. Yo sé lo que la ruta de inducción dice, y cómo se utiliza. Lo que no sé es su 'estado': es un teorema? un axioma? Algo que es familiar para el tipo de teóricos, pero no tiene una fácil interpretación para un matemático? Sé que el camino de la inducción es 'el principio de inducción para los tipos de identidad', pero eso no significa que está incluido como parte de la definición de la identidad?

Cualquier ayuda es apreciada.

Answer 1

El univalence axioma es que no pretende comprimir o ignorar el tipo de equivalencias entre los dos tipos diciendo que sólo pueden venir de una identificación. Sus efectos van más bien al revés. Se explica cuál es el tipo de identidad de un universo que se está diciendo que la búsqueda de una equivalencia es exactamente lo que tienes que hacer para encontrar una identificación entre dos tipos. Para todos ustedes saben (y como usted menciona), a un universo que no satisface univalence podría ser un conjunto. Así que usted puede tomar el punto de vista de que en lugar de ignorar las equivalencias de la univalence axioma se está inflando tipos de identidad de una manera muy precisa.

Hay una muy buena razón para requerir univalence, y es encontrar un montón de tipos de familias. Tomando el punto de vista de que un tipo de familia más de un tipo es la expresión de una propiedad de ese tipo, sería una vergüenza si no podíamos ser expresiva, utilizando el tipo de familias. Una familia de tipos puede ser visto como una función en el universo. Dado que las funciones han de preservar las identificaciones y debido a que a veces tienen que demostrar explícitamente que su construcción de la familia conserva identificaciones (por ejemplo, cuando su toma de una familia de más de un HIT), entonces el univalence axioma viene en muy práctico porque ahora usted sabe que usted puede encontrar una identificación entre dos tipos mediante la búsqueda de una equivalencia en su lugar.

Para responder a su segunda pregunta: en homotopy tipo de teoría, tipos de identidad tiene la condición de básica, de constructor de tipo (como es el estado de dependiente de la función de tipos, también) y el principio de la inducción (o dependiente de la eliminación de la regla) viene con ellos. Por lo que simplemente se supone que estar presente. Eso es todo, tan lejos como el libro de que se trate.

Pero hay personas que buscan modelos de teoría tipo con tipos de identidad. Por ejemplo, Awodey interpretado tipos de identidad por medio de la factorización de la diagonal $A\to A\times A$ a un trivial cofibration seguido por un fibration (este sería el "fácil" de interpretación para un matemático, al menos si la (s)está trabajando con Quillen las estructuras del modelo). Mostrando que el objeto a través del cual esta diagonal factores, en efecto, el principio de la inducción de tipos de identidad es un teorema.

Answer 2

El univalence axioma es mejor entendido como la definición de lo que significa para los dos tipos son iguales. En virtud de las proposiciones-como-tipos principio, un término de tipo de $A = B$ es una "prueba" de que el $A$ $B$ son iguales; y la mayoría de los matemáticos dicen que esta "prueba" es precisamente una de equivalencia (o isomorfismo) entre $A$$B$.

Desde el camino de la inducción de los rendimientos de una función canónica $(A = B) \to (A \simeq B)$, es natural preguntarse que esta función sea una equivalencia. No nos limitamos a pedir una función de $(A \simeq B) \to (A = B)$ porque queremos saber que las dos construcciones son mutuamente inversas (hasta algo más de las igualdades), de modo que el tipo de $A = B$ es determinado (hasta equivalencia).

Vale la pena señalar que, en ausencia de univalence, es posible que el único término de tipo de $A = B$ (proporcionalmente) igual a $\mathsf{refl}$ (y, en particular, dispone de un plazo de tipo de $A = B$ implica $A \equiv B$).

Como para la ruta de acceso de la inducción en el ordinario (es decir, prueba irrelevante) matemáticas: en cierto sentido, corresponde a la indiscernibility de identicals, pero que es tan obvio como para ser casi sin sentido.