Bibliografía del tratado

Fecha de última modificación

1 de octubre de 2026

Índice del tratado

La bibliografía distingue pasajes cotejados, metadatos y referencias de contexto. No se declara lectura integral de una obra a partir de su ficha, resumen o índice. Los pasajes que aún requieren colación se indican expresamente. La evidencia de código y CI se consulta por separado en el apéndice D.

Libros, artículos y notas de autor

Asperti–Longo

Andrea Asperti y Giuseppe Longo. Categories, Types and Structures: An Introduction to Category Theory for the Working Computer Scientist. MIT Press, 1991. Texto autorizado en el sitio del autor.

Alcance de consulta: §2.7, Defs. 2.7.2–2.7.3 y Prop. 2.7.4, pp. 36–37; pasaje cotejado.

Awodey, Category Theory

Steve Awodey. Category Theory. Oxford University Press, 2006. Capítulo 8, Categories of Diagrams.

Alcance de consulta: Cap. 8, pp. 159–178; metadatos y rango editorial acreditados históricamente; localizador fino pendiente.

Awodey, Type Theory

Steve Awodey. Topics in Logic: Type Theory, curso 80-518/818, primavera 2025. Sitio del curso; Simple Type Theory, borrador fechado 20 febrero 2025.

Alcance de consulta: §2.2, Prop. 2.2.6 y Prop. 2.2.8, pp. 16–17: estructura de CCC; pasajes cotejados. §2.3, pp. 21–22 impresas: interpretación de tipos y contextos, aplicación mediante evaluación y abstracción por transposición; Def. 2.3.1 y Prop. 2.3.2, p. 22, modelo y corrección ecuacional por inducción, cotejadas. §2.5, Teorema 2.5.2 y Cor. 2.5.3, pp. 31–33: formulación de biequivalencia entre teorías lambda y CCC pequeñas, localizada; el borrador omite parte de la verificación de los funtores inversos, por lo que no se le atribuye una prueba íntegramente desarrollada ni una equivalencia de fundamentos completos.

Brattka

Vasco Brattka. Computability over Topological Structures. Manuscrito de autor; el ejemplar anuncia publicación futura en Computability and Models. PDF del autor.

Alcance de consulta: Defs. 2.1, 2.3 y 3.1, pp. 3, 5 y 8; cotejadas. No se atribuye al manuscrito la fecha de una edición posterior sin verificar.

Chapman–Uustalu–Veltri

James Chapman, Tarmo Uustalu y Niccolò Veltri. «Formalizing Restriction Categories». Journal of Formalized Reasoning 10(1), 2017, pp. 1–36. DOI 10.6092/issn.1972-5787/6237.

Alcance de consulta: §§2.1–2.2, Defs. 1–3 y Lema 1, pp. 3–4; pasajes cotejados. Formalización externa en Agda, no Lean del tratado.

Enderton, conjuntos

Herbert B. Enderton. Elements of Set Theory. Academic Press, 1977; ejemplar consultado: impresión digital transferida en 2009, ISBN 978-0-12-238440-0. Editorial.

Alcance de consulta: Cap. 3, Functions, pp. 42–44: definición de función como relación univaluada (p. 42), tipado \(A\to B\), dominio e imagen (p. 43), composición, restricción e imagen directa (p. 44); pasajes cotejados. Enderton identifica la función con la relación y no incorpora un codominio único al conjunto de pares: el tratado declara separadamente su contrato tipado. Página legal también cotejada.

Enderton, computabilidad

Herbert B. Enderton. Computability Theory: An Introduction to Recursion Theory. Academic Press, 2011, ISBN 978-0-12-384958-8. Editorial.

Alcance de consulta: Cap. 3, p. 67, obstrucción diagonal: acreditado en TF-BIB-P2a. Citas amplias a caps. 1–4: localizadores finos pendientes.

Gran

Marino Gran. Notes on regular, exact and additive categories. Summer School on Category Theory and Algebraic Topology, EPFL, 11–13 septiembre 2014. PDF institucional.

Alcance de consulta: §1.1, Defs. 1.1.5–1.1.6 y Prop. 1.1.7, pp. 5–6: definiciones y prueba de regular epi ⇒ strong epi, cotejadas. §1.2, pp. 7–9, Def. 1.2.2 / Ejemplos 1.2.3: factorización por cociente del par núcleo en Grp y estabilidad de sobreyecciones por pullback; pasajes cotejados, localizador del fundamento externo de TF-CEX-00003. No se usa su observación sobre escisión en Set como teorema sin AC.

Heunen–Tull

Chris Heunen y Sean Tull. «Categories of Relations as Models of Quantum Theory». Electronic Proceedings in Theoretical Computer Science 195, 2015, pp. 247–261. DOI 10.4204/EPTCS.195.18. Manuscrito de los autores.

Alcance de consulta: §2, Defs. 2.1 y 2.3, pp. 3–4 del manuscrito; cotejo localizado. Rango de revista verificado en el registro arXiv de los autores; no se traslada automáticamente la paginación del manuscrito a la revista.

Kavvos

G. A. Kavvos. On the Semantics of Intensionality and Intensional Recursion. DPhil, University of Oxford, 2017. DOI 10.5287/ora-y5zrveqnm. Registro institucional.

Alcance de consulta: §2.1.2, Teorema 6; acreditado en TF-BIB-P2a. No se declara lectura integral.

Kurz

Alexander Kurz. Regular and Exact Categories. Notas web en construcción. Texto del autor.

Alcance de consulta: Contexto auxiliar, no autoridad única de definición; consulta histórica delimitada en TF-BIB-0001.

Lawvere

F. William Lawvere. «Diagonal Arguments and Cartesian Closed Categories» (1969), reimpresión con comentario del autor en Reprints in Theory and Applications of Categories, n.º 15, 2006, pp. 1–13. Texto de la revista.

Alcance de consulta: Teorema 1.1 y Corolario 1.2, p. 5; pasaje cotejado. No confundir número de reimpresión con volumen de la revista principal.

Lee

Sori Lee. Subtoposes of the Effective Topos. Tesis de maestría, Utrecht University, agosto 2011. Versión arXiv:1112.5325v1.

Alcance de consulta: portada y §1.2.4, Def. 1.2.21 y Prop. 1.2.22, pp. 22–23 impresas (páginas 23–24 del PDF), cotejadas: aplicaciones parciales mediante subobjetos, propiedad universal por pullback y construcción del clasificador mediante subobjetos subterminales del objeto potencia. La proposición remite su prueba a la teoría elemental de topoi; no se le atribuye una demostración desarrollada en el texto. Referencia ya citada en el capítulo 8, incorporada a esta consolidación.

Lawvere–Rosebrugh

F. William Lawvere y Robert Rosebrugh. Sets for Mathematics. Cambridge University Press, 2003. DOI 10.1017/CBO9780511755460.

Alcance de consulta: §§4.2–4.3, pp. 80–85, Def. 4.5 y Prop. 4.14: cotejados. §3.3, Def. 3.23 y Prop. 3.25, pp. 64–65: gráficas y recuperación; §3.4, Def. 3.29, p. 66: igualador; §5.1, pp. 96–98, y §5.2, pp. 98–100: correspondencia universal y evaluación/currificación; pasajes cotejados. §1.1, Notación 1.1, p. 2: dominio y codominio tipados; §1.3, Defs. 1.4–1.6, p. 8: sobreyección, inyección y biyección; §1.4, Def. 1.13, pp. 10–11: categoría; §1.5, Def. 1.14 y axioma de separación por 1, pp. 11–12: cotejados. §2.2, Defs. 2.6 y 2.11, pp. 32–33: mono y parte; §2.3, Defs. 2.13 y 2.15, p. 34: inclusión y pertenencia; §2.4, Def. 2.20 y axioma de representación por valores de verdad, pp. 38–39: cotejados. §2.5, Def. 2.26, p. 40 y caracterización de preimagen, pp. 41–42; §3.5, Def. 3.35 y Prop. 3.36 con prueba, pp. 69–70: cotejados. La separación por puntos y el clasificador 2 son propiedades especiales de los conjuntos abstractos; no se trasladan a toda categoría. §1.2, axioma del terminal y Def. 1.3, pp. 6–7: elemento como flecha desde 1 y evaluación como composición, cotejados. Del capítulo 8 citado por el capítulo 3 del tratado se cotejó el pasaje introductorio de §8.1, p. 136: \(2^X\) como potencia de conjuntos abstractos mediante funciones características; no se le atribuye aquí una prueba de existencia para todo marco categórico ni lectura integral del capítulo.

McLarty

Colin McLarty. Elementary Categories, Elementary Toposes. Oxford University Press, 1992. DOI 10.1093/oso/9780198533924.001.0001. Basics, capítulo 13, pp. 117–125, DOI 10.1093/oso/9780198533924.003.0014.

Alcance de consulta: Cap. 13, Basics, pp. 117–125: identidad, DOI, rango y resumen editorial verificados. El resumen formula la definición de topos/clasificador; no se atribuye lectura del capítulo completo ni cotejo de sus pruebas. Fuente de contexto en §7.7; el contrato utilizado está escrito en el tratado.

Naylor

Daniel Naylor. Category Theory, notas, §7, Regular Categories. Sitio del autor.

Alcance de consulta: Definición de categoría regular; cotejo histórico registrado. Año del ejemplar no establecido.

Pauly–Steinberg

Arno Pauly y Florian Steinberg. «Comparing Representations for Function Spaces in Computable Analysis». Theory of Computing Systems 62, 2018, pp. 557–582; publicación en línea 2017. DOI 10.1007/s00224-016-9745-6.

Alcance de consulta: §1.2, Def. 1: representación como sobreyección parcial desde el espacio de Baire y realizador de función multivaluada bajo promesa de dominio; pasajes cotejados en el texto editorial HTML y pp. 3–4 del PDF de publicación anticipada alojado por Cambridge. La definición no prescribe comportamiento fuera de los nombres válidos del dominio. El mismo apartado describe nombres métricos mediante aproximaciones con error acotado por \(2^{-n}\). §1.3, Def. 3: reducibilidad de Weihrauch, distinta del mero cambio de representación; no se identifica con la relación de traducción del tratado. PDF de publicación anticipada.

Spivak

David I. Spivak. Category Theory for Scientists. Versión docente MIT OCW, 2013. PDF del curso.

Alcance de consulta: §5.2.1.22, Def. 5.2.1.23, p. 225: clasificador de subobjetos en categorías de funtores; pasaje cotejado. Se conserva la versión docente, sin extrapolar páginas a ediciones posteriores.

Stekelenburg

W. P. Stekelenburg. Realizability Categories. Tesis doctoral, Utrecht University, 2013. Registro institucional.

Alcance de consulta: Fuente de contexto; autor y condición doctoral acreditados. Sin pasaje de prueba importado por el tratado.

Trimble

Todd Trimble. An elementary approach to elementary topos theory. Texto del autor.

Alcance de consulta: Teorema A topos is a regular category y demostración siguiente, tramo sobre cocientes y exactitud: resultado externo utilizado en caps. 4, 7 y 17. Texto completo recuperado del sitio del autor el 30-09-2026; cotejo delimitado al teorema y su prueba sobre regularidad, después del teorema de coigualación de equivalencias. La prueba usa límites finitos, coigualadores y preservación por pullback vía cierre cartesiano local; no se atribuye lectura íntegra de las notas.

HoTT

The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. Sitio oficial del libro.

Alcance de consulta: §1.2, pp. 28–30: tipos función, aplicación, abstracción y reglas beta/eta; §2.9, Axioma 2.9.3, pp. 104–105: extensionalidad como equivalencia de happly; §4.9, Teoremas 4.9.4–4.9.5 y sus pruebas, pp. 178–180: univalencia implica extensionalidad débil, que implica extensionalidad. Pasajes cotejados en el ejemplar privado. No se extiende esta lectura al libro completo.

Weihrauch

Klaus Weihrauch. Computable Analysis: An Introduction. Springer, 2000. DOI 10.1007/978-3-642-56999-9.

Alcance de consulta: Metadatos editoriales reconfirmados. Cap. 3, Naming Systems, pp. 51–84 y cap. 4, Computability on the Real Numbers, pp. 85–122, rangos del índice editorial cotejados; no se declara lectura de esos capítulos ni localización de una prueba a partir del índice. Localizadores finos no verificados; referencia de contexto para §§9.4 y 10.5, cuyas definiciones y reducciones se escriben íntegramente en el tratado y se contrastan con Pauly–Steinberg.

Weihrauch–Wu–Ding

Klaus Weihrauch, Yongcheng Wu y Decheng Ding. «Absolutely non-computable predicates and functions in analysis». Mathematical Structures in Computer Science 19(1), 2009, pp. 59–71. DOI 10.1017/S096012950800724X.

Alcance de consulta: Metadatos y resumen editorial cotejados; pasaje de prueba no colacionado. Fuente de contraste, no sustituto de las reducciones escritas en el capítulo 10.

Recursos de contraste y documentación

Trece recursos secundarios de contraste y una documentación histórica de software, sin duplicar los alias de una misma entrada. Consulta: 30-09-2026. Los alcances de cada cotejo se precisan a continuación; no sustituyen las pruebas internas.

  • CategoryTheory/Limits/Presheaf. Mathlib histórico. Documentación histórica alojada por IISc: tautologicalCocone e isColimitTautologicalCocone. No acredita CI ni Lean general del tratado.
  • Pregunta 1650277 sobre clasificadores de subobjetos en órdenes parciales. Recurso. Math StackExchange; acceso HTTP 403, autoría y respuesta no verificadas. Contexto; TF-CEX-00002 se prueba internamente.
  • nLab. Rel. Recurso. Recurso colaborativo secundario; apartados cotejados delimitados en la bibliografía del tratado. No se atribuye una fecha de publicación no establecida.
  • nLab. Axiom of choice. Recurso. Recurso colaborativo secundario; apartados cotejados delimitados en la bibliografía del tratado. No se atribuye una fecha de publicación no establecida.
  • nLab. Choice object. Recurso. Recurso colaborativo secundario; apartados cotejados delimitados en la bibliografía del tratado. No se atribuye una fecha de publicación no establecida.
  • nLab. Co-Yoneda lemma. Recurso. Recurso colaborativo secundario; apartados cotejados delimitados en la bibliografía del tratado. No se atribuye una fecha de publicación no establecida.
  • nLab. Equivalence of categories. Recurso. Recurso colaborativo secundario; apartados cotejados delimitados en la bibliografía del tratado. No se atribuye una fecha de publicación no establecida.
  • nLab. Partial function. Recurso. Recurso colaborativo secundario; apartados cotejados delimitados en la bibliografía del tratado. No se atribuye una fecha de publicación no establecida.
  • nLab. Partial map classifier. Recurso. Recurso colaborativo secundario; apartados cotejados delimitados en la bibliografía del tratado. No se atribuye una fecha de publicación no establecida.
  • nLab. Subobject classifier. Recurso. Recurso colaborativo secundario; apartados cotejados delimitados en la bibliografía del tratado. No se atribuye una fecha de publicación no establecida.
  • Bell, John L.. The Axiom of Choice. (2025). Recurso. Stanford Encyclopedia of Philosophy, edición verano 2025; revisión sustantiva del 10 de diciembre de 2021. Contraste secundario: sección 1, AC2–AC4.
  • Immerman, Neil. Computability and Complexity. (2021). Recurso. Stanford Encyclopedia of Philosophy; revisión sustantiva del 18 de octubre de 2021; contraste secundario, secciones 2.3–2.4.
  • Dean, Walter; Naibo, Alberto. Recursive Functions. (2024). Recurso. Stanford Encyclopedia of Philosophy; revisión sustantiva del 1 de marzo de 2024; contraste secundario, secciones 3.1–3.2.
  • Dybjer, Peter; Palmgren, Erik. Intuitionistic Type Theory. (2024). Recurso. Stanford Encyclopedia of Philosophy; revisión sustantiva del 23 de septiembre de 2024; contraste secundario, sección 3.8.

Cotejos localizados de recursos nLab

Se recuperó el XHTML de las páginas el 30-09-2026; la consulta se limita a los apartados siguientes. Son contrastes de pruebas internas, no fuentes primarias que las sustituyan.

  • Equivalence of categories: apartado Definitions, definición por cuasiinversos y proposición sobre plena fidelidad y sobreyectividad esencial escindida, con prueba; apartado Variants / Strong equivalence y advertencia sobre elección. Cotejo de §14.1 y TF-THM-00109. El texto distingue datos suministrados de la mera existencia de representantes; su prueba recíproca utiliza identidades triangulares. La prueba del tratado trata también isomorfismos naturales inicialmente no triangulares mediante su corrección beta.
  • Partial function: In category theory / In the category of sets; General abstract / In terms of spans / In terms of the maybe monad; The category of sets and partial functions. Cotejo del span monomórfico, igualdad por isomorfismo de dominios y codificación etiquetada clásica de §14.2, TF-THM-00110; no se atribuye la suma binaria a dominios constructivos arbitrarios.
  • Co-Yoneda lemma: Every presheaf is a colimit of representables, proposición y prueba, para base pequeña; especialización a Set. Cotejo de las fórmulas de colímite sobre la categoría de elementos y coextremo, TF-THM-00127 / TF-THM-00129. No acredita Lean general ni efectividad de los cocientes.

Colación adicional de recursos y fundamento externo — 30-09-2026

  • nLab, Rel: Definition y Relations in a category, contraste de composición conjuntista e imagen del pullback en categorías regulares (§§3.5/4.3/13.1). La fórmula impresa del recurso tiene un subíndice intermedio ambiguo; se conserva la formulación tipada interna del tratado, no se copia esa notación.
  • nLab, Axiom of choice: In set theory e In other categories / External form, formulación de escisión y distinción entre epi y epi regular. Choice object: Definitions and terminology / Properties, distinción entre objeto proyectivo (índices) y objeto de elección (valores). Contraste de §5.2; no se importan sus afirmaciones adicionales sobre buena ordenación.
  • nLab, Partial map classifier: Definition, proposición universal y prueba, Constructions; cotejados spans, clasificación por pullback, caso booleano/extensivo y construcción por subsingletons en un topos. Contraste de §§6.6/8.1–8.4; sin Lean atribuido.
  • nLab, Subobject classifier: Definition y Examples / In Set / In a non-boolean topos; cotejada condición universal y delimitación de Ω frente a 1+1. Contraste de §§3.3/7.5.
  • SEP, The Axiom of Choice, edición verano 2025: §1, formulaciones AC2/AC3/AC4; familias, relaciones totales y inversa derecha, cotejadas como contraste de TF-THM-00038 y C.19.
  • SEP, Recursive Functions: §3.1 Teorema 3.2, §3.2 diagonal parcial y Teorema 3.4 (Rice) con prueba, cotejados como contraste de capítulos 10–11. SEP, Computability and Complexity: §§2.3–2.4, decisión, enumerabilidad y diagonal de K, cotejadas. Ninguna página secundaria sustituye las reducciones internas.
  • SEP, Intuitionistic Type Theory: §3.8, extracción Pi/Sigma y advertencia de elección extensional en setoides; cotejo de §13.4 y C.22, conservando las reglas de igualdad propias del sistema declarado.
  • Documentación histórica Mathlib, módulo CategoryTheory/Limits/Presheaf: declaraciones CategoryTheory.tautologicalCocone y CategoryTheory.isColimitTautologicalCocone, tipos y comentarios cotejados. Es documentación de software, no certificación Lean del teorema general del tratado ni CI nuevo.
  • Math StackExchange, pregunta 1650277: acceso directo devuelve HTTP 403. Sin nuevo cotejo de la respuesta; permanece como contexto secundario no verificado. El contraejemplo Pos se prueba explícitamente en TF-CEX-00002.

La apertura de páginas y estos pasajes no se presenta como lectura integral de cada recurso. Los localizadores de libros todavía no verificados se conservan expresamente como tales.

Cierre de la auditoría bibliográfica de esta edición — 30-09-2026

El cierre consiste en identificar las fuentes de todos los usos del corpus, distinguir su función y registrar el respaldo de las afirmaciones utilizadas. Hay 23 entradas de libros, artículos y notas de autor, 13 recursos secundarios de contraste y una documentación histórica de software; 37 registros únicos. Los alias de Partial function se consolidan. La bibliografía maestra del sitio registra las mismas fuentes con claves TF; GitHub/CI sigue separado en el apéndice D.

El inventario de 26 documentos, la concordancia narrativa y la matriz de 269 resultados se han reconciliado. Los resultados externos utilizados —regularidad de topoi y Grp, y la relación univalencia/extensionalidad— tienen fuentes y localizadores cotejados. Las demostraciones de Yoneda, computabilidad y representaciones incluidas en el tratado se sostienen en sus argumentos y contratos explícitos, no en una supuesta lectura de libros inaccesibles.

Límites de lectura conservados, sin acreditación implícita: Awodey (2006), cap. 8; McLarty, texto completo de Basics; usos amplios de Enderton, caps. 1–4, y Weihrauch, caps. 3–4, no tienen nueva colación fina integral. Las fichas indican exactamente qué se pudo consultar. Math StackExchange no permitió leer la respuesta. Estos usos de contexto no se convierten en pruebas externas adoptadas; completar esas lecturas o incorporar nuevos resultados requeriría otra colación. El cierre de la auditoría no significa lectura íntegra de las obras ni elimina estos límites.

Colación complementaria: Trimble, apartado Slices of a topos: proposición sobre el adjunto derecho Pi_X y prueba por el objeto de secciones; observación posterior sobre adjuntos a ambos lados de f*. Internal universal quantification: proposición Universal quantification is right adjoint to pulling back y demostración por característica/transposición. Cotejo de la referencia contextual de §7.7; no lectura íntegra atribuida.

Reutilización

GFDL-1.3-or-later