Antes de intentar abordar sus preguntas específicas, permítanme darles un pensamiento que provoca la no-respuesta:
Revertir la matemática es imposible (e irrelevante) en HoTT!
Esto es debido a que HoTT apoya plenamente relevante de prueba de matemáticas, así que cuando usted se refiere a un teorema se refiere necesariamente a una prueba de ese teorema. La cuestión de si las hipótesis son necesarias no tiene sentido en este contexto, ya que las hipótesis son parte del teorema de sí mismo!
Ahora que sus pensamientos han sido provocados, permítanme corregir la declaración anterior:
HoTT no es el fin de revertir las matemáticas!
En realidad, sólo hace a la inversa (y constructiva) matemáticas de las preguntas más obvias. La mayoría de razón fundamental por la inversa de la matemática que existe es el increíble poder de la cuantificador existencial. En HoTT, que es inmediatamente obvio. Un plano existencial de la instrucción se interpreta como un dependiente de la suma del tipo de HoTT: "$\sum_{x:A} P(x)$ está habitado" es la forma correcta de decir que "hay un $x$ tipo $A$ tal que $P(x)$." Por definición, cada habitante $x:A$ de este tipo está equipado con una justificación de $P(x)$. Para obtener la costumbre, el cuantificador existencial, uno debe truncar $\sum_{x:A} P(x)$ a una proposición. Esto plantea la pregunta: ¿puede este truncamiento revertirse? ¿Cuáles son los necesarios hipótesis para revertir este truncamiento? Esto es lo inverso de matemáticas de preguntas se convirtió en la traducción a la lengua de HoTT. Nota cómo "matemáticas" en el reverso de pregunta de matemáticas se ha convertido! Esto no es ninguna sorpresa a la práctica de la inversa de los matemáticos, pero es muy interesante de cómo revertir la matemática se convierte en menos mítica en este contexto.
Ahora voy a agregar lo que yo sé acerca de cada una de sus preguntas. Como todavía estoy aprendiendo sobre HoTT, estas respuestas están lejos de ser completa ni definitiva. Espero que los expertos va a meter la cuchara en algún momento.
La anterior ordenación de las direcciones de esta pregunta. Una dificultad adicional es que parece que todavía hay mucho trabajo por hacer en la comprensión de los modelos de HoTT. La solidez y la integridad teoremas obtenidos por Awodey & Warren y Gambino & Garner está casi allí, pero Awodey señala algunos de los problemas más sutiles. No sé si estos problemas son bastante problemática a hacer que sea difícil establecer la no-provability resultados para HoTT.
HoTT es quizás demasiado fuerte para su uso como un sistema de base para el clásico de la inversa de las matemáticas. La razón es, básicamente, la misma razón por la ZF es a menudo demasiado fuerte para ese propósito. Nota, sin embargo, que incluso ZF no es completamente inútil. Por ejemplo, como testigo de una gran cantidad de literatura, ZF es un perfectamente bien la base de la teoría para el análisis de la elección de los principios. HoTT es más prometedora como un sistema de base constructiva inversa de las matemáticas, pero la constructivity de la univalence axioma es actualmente un problema abierto.
No creo que el univalence axioma es que la problemática. La ley de medio excluido siempre los enfrentamientos con las propuestas-como-tipos de interpretación. La forma correcta de formular la ley de medio excluido en HoTT es a restringir a las proposiciones — de los tipos con más de un elemento. Esta versión de la ley de medio excluido no entre en conflicto con univalence y captura todos los usos normales.
No creo que nadie se ha ocupado de la cuestión de si HoTT es un conservador extensión de BISH (decir) o cuán lejos está de ser un conservador de extensión.
Es difícil hacer una comparación. El sistema de base de RCA0 fue explícitamente diseñado para capturar básicos de la teoría de la computabilidad. HoTT no fue diseñado de esa manera, pero otros aspectos de la computabilidad eran importantes en el diseño de los componentes.
No le veo mucho aumento en el uso de la prueba de asistentes para revertir las matemáticas pero puede ser que sea miope.
Sí, algunos axiomas adicionales, tales como proposicional, cambiar el tamaño, la ley de medio excluido, y el axioma de elección se han analizado hasta cierto punto. HoTT es tan joven que muy poco de esto se ha hecho todavía.
