La mayoría de las definiciones de los números racionales como un tipo inductivo superior en la teoría de tipos homotópicos univalentes (como los de la biblioteca Agda cúbica, por ejemplo) requieren el uso de un conjunto cociente o un constructor de truncamiento 0. ¿Existe una manera de definir los números racionales como un tipo inductivo superior sin utilizar conjuntos cotizantes o el truncamiento 0?
Respuestas
¿Demasiados anuncios?
Una versión de la teoría de las fracciones continuas es la siguiente. Podemos definir las operaciones $S,T,J\colon\mathbb{Q}^+\to\mathbb{Q}^+$ por $S(x)=x+1$ y $J(x)=1/x$ y $T(x)=JSJ(x)=x/(x+1)$ entonces podemos definir $M$ para ser el monoide libre generado por $S$ y $T$ . Tenemos entonces un mapa de evaluación $M\to\mathbb{Q}^+$ dado por $m\mapsto m(1)$ y no es difícil comprobar que se trata de una biyección.
Si quisiéramos, podríamos darle la vuelta a esto y definir esencialmente $\mathbb{Q}^+$ para ser lo mismo que $M$ (y $\mathbb{Q}$ para ser $\{0\}\amalg\mathbb{Q}^+\amalg -\mathbb{Q}^+$ ). Esto hace que $\mathbb{Q}$ en un tipo inductivo. La ordenación en $\mathbb{Q}$ y la inclusión $\mathbb{Z}\to\mathbb{Q}$ funcionan bien en esta imagen, pero las operaciones algebraicas son incómodas.
También puede introducir el tipo $R$ de $2\times 2$ matrices $\begin{pmatrix} a&b\\c&d\end{pmatrix}$ con $a,c,d\in\mathbb{Z}^+$ y $b\in\mathbb{N}$ y $ad=bc+1$ . Dado un racional positivo $q\in\mathbb{Q}^+$ podemos escribirlo como $q=a/c$ con $\text{gcd}(a,c)=1$ . Esto significa que existe $b,d\in\mathbb{Z}$ con $ad=bc+1$ . Podemos cambiar el par $(b,d)$ sumando múltiplos de $(a,c)$ , por lo que hay que elegir con $0<d\leq c$ . De esto obtenemos $b=(ad-1)/c$ con $0<ad\leq ac$ donc $0\leq b<c$ . Esto demuestra que el mapa $\begin{pmatrix} a&b\\c&d\end{pmatrix}\mapsto a/c$ da una biyección $R\to\mathbb{Q}^+$ que es una versión de la respuesta de Noah Snyder. Creo que esto se puede hacer de forma bastante satisfactoria a partir de las definiciones inductivas, y que se puede utilizar la interacción entre $\mathbb{Q}^+$ y $R$ para definir las operaciones algebraicas sobre $\mathbb{Q}^+$ . Lo he hecho en parte en Lean pero hace tiempo que no pienso en ello y no recuerdo con precisión cuál era el estado de la cuestión.
maclema
Puntos
5959
Podrías intentar definirlos como triples de un entero, un entero positivo y una prueba de que esos dos enteros son relativamente primos.
(Es posible que me haya perdido algo técnico aquí sobre si las pruebas de que los pares son relativamente primos es ya una $(-1$ )sin ningún truncamiento, pero creo que debería estar bien).
