¿Cómo define categorías (infinito, 1) en la teoría de tipos de homotopía?

Question

Una de las principales motivaciones de Homotopy Tipo de Teoría es que, naturalmente, se basa en el mayor tipo de duda desde el principio. Un valor importante donde una mayor coherencia de los requisitos de ser molesto es el de mayor categoría de la teoría. Es fácil hablar de la $\infty$-groupoids en HoTT, sólo son de tipos y de construir ellos como superior inductivo tipos. ¿Cuál será el siguiente paso? ¿Cómo se puede hablar de $(\infty,1)$-categorías? Miré a mi alrededor en el nlab y los blogs relevantes, pero no encontró nada.

Lo natural es que la instalación tiene un tipo de objetos y (dependiente) tipo de morfismos. Pero la composición parece correr en todas las dificultades normales de la coherencia en la categoría superior a la teoría. ¿La HoTT punto de vista de simplificar las cosas a todos aquí?

Siéntase libre de asumir que estoy familiarizado con la discusión de ordinario categorías en la HoTT libro y el fondo en la HoTT libro. Por otro lado, también se supone que debo encontrar todas las definiciones de las categorías más altas, más allá de la dimensión 2, al menos un poco confuso. Mi motivación es que estoy tratando de entender lo que usted necesita hacer con el fin de dar una prueba formal de la cobordism hipótesis en la dimensión 1.

Answer 1

Este es un importante problema abierto. Hay varios imaginable enfoques, incluyendo pero no limitado a:

1. Imitar algunos de los más comúnmente utilizados homotopical definición de $(\infty,1)$-categoría dentro de HoTT. El candidato más probable parece ser completa Segal espacios, ya que tienen un espacio de objetos en lugar de un conjunto de objetos. Esto requeriría una definición de "simplicial de tipo" en la HoTT, que es otro importante problema abierto (que es motivar a algunas personas para intentar modificar el tipo de teoría).

2. El uso de una definición de un tipo más teórico de estilo. El $\infty$-groupoids de HoTT son naturalmente "algebraica" a la Grothendieck/Batanin, así que tal vez sería más natural utilizar de una manera similar algebraicas definición de $(\infty,1)$-categoría. Uno podría, por ejemplo, intentar codificar un operad de una adecuada ordenación con una definición inductiva.

3. Inventar una especie de "dirigidos tipo de teoría", cuyos objetos básicos se $(\infty,1)$-categorías, de la misma manera que los objetos básicos de HoTT se $\infty$-groupoids.

4. Aprovechar el hecho de que HoTT admite modelos no sólo en $\infty$-groupoids pero en otras $(\infty,1)$-toposes, señalando que completa segal espacios vivir dentro de la $(\infty,1)$-topos de simplicial espacios. He propuesto esta aquí; Andre Joyal independientemente tenido la misma idea.

En este punto yo no presumiría apuesta en la que el enfoque será el mejor, o si va a ser algo totalmente diferente.

Answer 2

Emily Riehl y Mike Shulman ahora tienen una preimpresión que crea una versión de la teoría de tipos que incluye$(\infty,1)$ - categorías como ciertos tipos de tipos.

Answer 3

Si bien esta pregunta tiene una respuesta aceptada, permítanme mencionar que ahora hay una preimpresión de James Cranch sobre cómo hacer categorías estructuradas sobre tipos de homotopía, es posible que le interese echar un vistazo.