¿Acercarse a la Teoría de Tipos y a la Teoría de Categorías como punto de partida en el estudio de las matemáticas?

Question

Soy un estudiante de Ingeniería Informática, con interés en Teoría de Tipos y Teoría de Categorías y tengo una pregunta más pedagógica/filosófica sobre estas áreas.

Parece que muchos investigadores en Teoría de Tipos y Teoría de Categorías en general, especialmente en Teoría de Tipos de Homotopías, ven sus áreas como un buen punto de partida para que cualquier estudiante aprenda matemáticas. Su punto de enfoque filosófico parece ser la exclusión completa de la teoría de conjuntos al principio de los cursos de matemáticas, en favor del enfoque constructivista/teoría de tipos.

Por lo que ya he leído, esta idea también parece buena para los cursos de informática, pero tiene un coste, que es el tema de esta pregunta: como no matemático, todos los intentos de tender un puente entre los principiantes, también llamados por Terrence Tao "la etapa pre-rigorosa" y estas zonas parecen infértiles.

Por ejemplo: el único libro realmente "apto para principiantes" sobre teoría de categorías es, con diferencia, Teoría de categorías para programadores por Bartosz Milewski. El libro de Steve Awodey, aunque afirma que es "para todos los demás", está, intencionadamente, lleno de ejemplos de estructuras matemáticas superiores que complican más que simplifican su contenido.

Y no sirve como libro para principiantes por otra razón: supone una madurez matemática más avanzada (lo que Tao podría definir como madurez de "etapa rigurosa"), que en muchos lugares (como Brasil, donde vivo) se desarrolla en cursos más centrados en conjuntos como Análisis, Topología, etc.

Tengo fe en la intención, así que mi pregunta es más en términos de: ¿Qué libros recomendarías sobre Teoría de Categorías y Teoría de Tipos que le hagan a uno pasar de "pre-riguroso" a "riguroso", es decir, aprender a demostrar cosas mientras se aprenden matemáticas como se aprende en Análisis, y suponiendo que no hay antecedentes (en absoluto)? ¿Existe un libro así?

Y más aún: si usted fuera profesor en un curso de introducción a las matemáticas y quisiera enseñar a personas que acaban de salir de la escuela en qué consisten las matemáticas utilizando sólo Teoría de Categorías y Teoría de Tipos, ¿qué libro utilizaría?

Answer 1

Descargo de responsabilidad: lo que sigue es subjetivo y, por supuesto, las opiniones pueden diferir.

No creo que tenga sentido intentar "aprender matemáticas" aprendiendo teoría de categorías, ya que pone el carro delante del caballo.

Hay muchos ángulos desde los que se puede llegar a la teoría de categorías: Puede que la teoría clásica de categorías le resulte un lenguaje unificador útil para estructuras básicas como los grupos abelianos, los espacios vectoriales, etc. Puedes venir desde el punto de vista de la CS, aprendiendo sobre sistemas de tipos cada vez más expresivos, reflexionando sobre el significado de la igualdad, y acabar estudiando HoTT, conociendo a otros que llegaron allí en busca de una aproximación sintética a la teoría de homotopías. O puede que te disguste que los fundamentos de la teoría de conjuntos te permitan preguntarte "¿Es $e\in\pi$ ?" y considerar el ETCS como una salida atractiva. La lista continúa.

En todos estos ejemplos se acaba aprendiendo algún aspecto de la teoría de categorías (véase "Bocetos de un elefante"), pero todos tienen en común que la teoría de categorías responde a una pregunta: si se desecha la pregunta, pierde sentido. Por ejemplo, ¿qué se supone que debe hacer un estudiante de primer año con la noción de categoría abeliana si antes no se ha encontrado con los ejemplos concretos de, por ejemplo, espacios vectoriales y grupos abelianos?

A veces tengo la impresión de que los jóvenes estudiantes consideran, con asombro, que la teoría de categorías es el "santo grial" de las matemáticas. En mi opinión, en realidad no lo es, al menos en lo que se refiere a la teoría clásica de categorías: Las ideas se dan sobre todo en ejemplos concretos, mientras que la teoría de categorías es extremadamente valiosa (esencial, de hecho, diría yo) para distinguir entre generalidades y especificidades. Pero, en palabras de uno de mis profesores de antaño: "No basta con decir 'morph morph' todo el tiempo".

Como alguien que se doctoró en teoría de categorías (homotópica) y que ahora utiliza fundamentos lógicos de teoría de tipos todos los días, mi consejo a los jóvenes estudiantes sería: Familiarízate con los diferentes aspectos de la teoría de categorías, y disfruta y abraza su generalidad y claridad conceptual, pero haz esto junto a no en su lugar, la adquisición de una sólida formación matemática "clásica".

Answer 2

Aunque yo mismo no he logrado entender ninguno de los dos temas a un nivel satisfactorio, puedo recomendar algunos libros que permitirían a alguien suficientemente inteligente lograrlo:

1. Teoría de la gavilla a través de ejemplos por Daniel Rosiak

Esto va a través de la teoría de categorías desde el punto de vista de la filosofía, por lo que es tan puro como usted puede conseguir. La ventaja es que también introduce la topología desde los fundamentos.

2. Eugenia Cheng La alegría de la abstracción

Este tiene más o menos un alto solapamiento de contenido con el primer libro, pero me pareció que las primeras secciones son más fáciles para alguien para conseguir lo que ct se trata.

También hay algunas cosas misc como Tom leister notas y así sucesivamente que todavía le ayudará. También puede comprobar los catsters en youtube.

---

Aparte de Bartosz Milewski, no he encontrado ningún buen recurso que analice el vínculo entre teoría de tipos y teoría de categorías desde el punto de vista de la programación.

Si eres como yo, probablemente te apetezca estudiar un poco de Haskell. Quizás relevante CS SE post

Sin embargo, le garantizo que quedará decepcionado. A la mayoría de la gente que hace programación funcional no le importa/no conoce en absoluto la teoría de categorías. También me parece que algo de Lambda Calculus es más importante en lo que respecta a la aplicación, y si usted pasa un poco más de tiempo, usted encontrará que algo aún más esotérico se puede ver que tienen fundamentos para el cálculo lambda, combinadores . Stephen Wolfram había escrito un libro sobre esto, pero me pareció demasiado molesto de leer, ya que era realmente un anuncio del lenguaje wolfram en forma oculta. Parece que se han creado algunos vídeos en youtube sobre el tema, así que puedes echarle un vistazo.

De todas formas, también puedes consultar el libro Homotopy type theory. El tema es diferente, pero las primeras secciones tratan la esencia de la teoría de tipos (o al menos lo intentan). He descubierto que a algunas personas que conozco personalmente tampoco les gusta mucho este libro, así que cada cual con sus preferencias.

La madriguera del conejo es extraordinariamente profunda y en algún momento te cuestionarás si las matemáticas tienen algún fundamento... ver este post de reddit

---

Por último, me gustaría señalar que, si bien la teoría de categorías puede captar bien las nociones topológicas (véase el libro de Tai danae Bradley), parece ser poco útil para comprender el análisis de cosas con derivadas. La experiencia personal y las conversaciones con algunos expertos me han llevado a la conclusión de que los métodos generales de la tc no se pueden adaptar para explicar la mayoría de las cosas del análisis, requiere mucha especialización . Pero, creo que hay algún esfuerzo para tender un puente sobre el vínculo todavía, recuerdo haber visto un artículo donde la integral de lebesgue es introducida por ct ( aunque nunca lo leí yo mismo).

Answer 3

Como físico que aprendió por sí mismo los fundamentos de la teoría de categorías (con ayuda de teóricos de categorías), intentar aprender matemáticas a partir de la teoría de categorías suena horrible. Sospecho que hay una suposición tácita por parte de aquellos que dicen que deberías aprender teoría de categorías para aprender matemáticas de que estás sólidamente en la fase rigurosa de tu educación, o que ya estás empezando a ser post-riguroso. Para el contexto de mi nivel de habilidad, probablemente estoy en algún lugar entre esos niveles en matemáticas (y post-riguroso en la física que probablemente me permite golpear por encima de mi peso).

Sin embargo, lo que he descubierto al tratar de utilizar la teoría de categorías es que la mayor ventaja es conectar campos diferentes y ver en qué se parecen, y a partir de ahí se puede obtener una intuición post-rigorosa diciendo que estas dos estructuras matemáticas tienen propiedades similares o las mismas propiedades de teoría de grupos, por lo tanto mi intuición de una se transfiere a la otra. Esto podría significar que una prueba bien conocida en la categoría X se puede trasladar a la categoría Y porque tienen las mismas herramientas básicas que utiliza la prueba. O puedes ver que la demostración de X et al es esencialmente la misma que la demostración de Y et al. Pero, en general, cualquier cosa que puedas demostrar con la teoría de categorías, puedes demostrarla utilizando herramientas especializadas para tu tema en particular.

Hay ejemplos contrarios a esta afirmación, en los que el uso de la teoría de categorías hace que una prueba sea más limpia de maneras que no son obvias en el marco original. El mejor ejemplo es que los grupos de homotopía superior son abelianos es mucho más elegante con sólo hablar de ello como un functor entre dos categorías y asumiendo una sola propiedad de la categoría básicamente hace que esta prueba de unas pocas líneas y más fácil de creer, mientras que la prueba original es de varias páginas de largo. Estoy seguro de que otros que conocen el campo pueden dar más ejemplos de dónde la teoría de categorías simplifica las pruebas o demuestra cosas desconocidas anteriormente.

Lo que me ha resultado útil en mi vida cotidiana al aprender la teoría de categorías no han sido las herramientas en sí, sino la forma de pensar que hace que abstraer cosas me resulte mucho más natural. Aunque esto también podría deberse en parte a que me vi forzado a desarrollar un pensamiento post-riguroso para comprender lo que estaba intentando enseñarme (habiendo sido bastante cómodamente riguroso cuando empecé a aprender teoría de categorías). En cuanto a las referencias, yo diría que las conferencias podrían ser más útiles si quieres aprender teoría de categorías, tal vez este curso que fue guiado más por ingenieros para ingenieros https://applied-compositional-thinking.engineering/ (aunque era sólido para las cosas básicas y contaba con un teórico de la categoría). También podría ser interesante echar un vistazo a algunas de las charlas de la conferencia sobre teoría de categorías aplicada ( https://msp.cis.strath.ac.uk/act2022/ ) pero muchos probablemente asumen un nivel de habilidad mucho mayor, pero había algunos sobre programación (por ejemplo, James Fairbanks como coautor) que podrían dar algunas ideas ya que vienes de la ingeniería/programación.