imagina una cosa que desenreda automáticamente definiciones matemáticas hasta la teoría de conjuntos, como la Sección 3.2 de Stacks comienza a hacer para un Esquema, como una forma de definir recursivamente cada concepto que podrías no conocer alguien codifique esto o lo que sea que hacemos nosotros, simios informáticos, estos días

con un límite de profundidad arbitrario o algo así, no es necesario llegar a ZFC o a alguna lógica matemática profunda. Solo un par de niveles hacia abajo podrían ayudar. Obviamente, algunas cosas (como los esquemas) se ramifican de manera loca, así que tendrías N ramas yendo hacia abajo recursivamente, pero sí.

si no es útil, ¿quizás bonito?

¿Quizás bajar a las definiciones de mathlib para el mínimo absoluto?

honestamente siento que me estoy violando a mí mismo al publicar en el TL y no solo para suscriptores, pero he estado olvidando hacer clic en el menú desplegable estos últimos 2 días, así que que le den.