En la HoTT de Cauchy Reales

Question

En el Homotopy Tipo de Libro de la Teoría no es una construcción dada de una especie de Cauchy reales a través de más de tipo inductivo y los autores comentó, que esta construcción es preferible a otras nociones (reales como setoid, una cierta cantidad de elección, dedekind reales). Me gustaría tener algo de información general sobre este tema:

1. Alguien puede explicar en términos sencillos (sin asumir ningún tipo de conocimiento de teoría tipo, digamos homotopy tipo de teoría) lo que el general de la intuición detrás de esta estructura es y cómo se relaciona con otros enfoques para el análisis (por ejemplo, el Clásico, el Obispo, Robinson No estándar, Suave diferencial, Computable, etc.)?
2. Es alguien realmente (sustancialmente) que trabajan con estos Cauchy reales? De nuevo en relación a otros tipos de análisis: ¿hay razones para creer que este es un aspecto realmente importante de la estructura (no "sólo" otro tipo de análisis no estándar)?

Answer 1

Juan explica de una forma de pensar acerca de la diferencia, de manera constructiva, entre Cauchy y Dedekind reales. ¿Qué hay de nuevo en el Cauchy reales en la HoTT Libro es que, a diferencia de la definición habitual de Cauchy de reales en la construcción de las matemáticas, que son de Cauchy completa en la que cada Cauchy secuencia de Cauchy reales converge. Puede resultar sorprendente que la definición habitual es insuficiente para garantizar este; el punto es que como normalmente se definen, cada uno de Cauchy real es una clase de equivalencia de Cauchy secuencias de racionales, así que si usted tiene un Cauchy secuencia de Cauchy reales elegir una representación de Cauchy secuencia para cada término en antes de que usted pueda "diagonalize" para encontrar un límite, y, en general, que requiere contables elección. El éxito de Cauchy reales de eludir este problema "haciendo el quotienting al mismo tiempo que la generación de Cauchy sequneces"; puede ordenar de pensar en ella como forma iterativa la adición de los límites de las nuevas secuencias de Cauchy mutuamente de forma recursiva con el pasar de los a de clases de equivalencia de secuencias de Cauchy.

A mi conocimiento, nadie ha perseguido esta idea de Cauchy número real mayor.

Answer 2

Para la primera pregunta, me parece más útil manera de pensar acerca de la la diferencia entre el Cauchy y Dedekind reales en HoTT para estar en condiciones de su estructura topológica. Si pensamos en un tipo de HoTT como un espacio, a continuación, el tipo de Dedekind reales es el espacio de los reales equipado con su estándar estructura topológica. Esto tiene sentido, dado que la norma topológico la estructura de los reales es inducida por los intervalos que utilizamos para definir Dedekind reales, así que dejamos que topológica de la información cuando se construyó ellos. El Cauchy reales, por otro lado, están los reales equipado con el discretos topología. Desde el GOLPE de Cauchy reales incluye un proposicional el truncamiento, estamos eliminando la topológica de la información que proviene de la Cauchy secuencias en la definición. Esta interpretación también tiene sentido de Lema 11.4.1 en la HoTT Libro. Siempre esperamos a (continua) de la función $\mathbb{R}_{c} \to \mathbb{R}_{d}$, ya que cada función de un discreto topológica del espacio es continuo. Sin embargo, nosotros sólo esperamos a (continua) la función va para otro lado cuando tenemos información adicional que nos permite "romper" la continuidad de la restricción, que es lo que Eq. 11.4.2 de la HoTT Libro no. Todo esto puede ser hecho preciso el uso de cohesiva HoTT, donde $\mathbb{R}_{c} = \flat\mathbb{R}_{d}$. Pero estamos en busca de seguir con una laico de explicación.

No sé si alguien está sustancialmente de trabajo con la de Cauchy de reales en HoTT. En la habitual fundamentos de Cauchy y Dedekind construcciones coinciden, pero esto se basa en el axioma de (contables) la elección. Si estamos pensando internamente, entonces el Cauchy reales de pop-up cada vez que estamos trabajando con los números reales como un conjunto, sin la topología usual.