He desnatada a través de una encuesta realizada por Thierry Coquand en univalentes fundaciones. Se afirma que "groupoids son más fundamentales que las categorías". Y que las categorías pueden ser vistos como groupoids equipado con una especie de pre ordenado de la estructura. Ver aquí, pp 41-45. Pero yo no entiendo muy bien los detalles de esta construcción. Es posible explicar este clásico de las matemáticas? Es decir, ¿existe una definición de una categoría (en el sentido clásico) en términos de un groupoid con una estructura adicional? La HoTT libro define las categorías directamente sin el uso de groupoids.
Respuestas
¿Demasiados anuncios?
Alan Storm
Puntos
506
No estoy seguro de si esto es lo que usted está buscando, o si este es el conocimiento básico para usted. Pero, en el Tipo de Teoría que cada tipo tiene la estructura de una $\infty$-groupoid. Dados dos elementos de un tipo $a,b:A$, tenemos un tipo de identidad $a=_Ab$ que expresa el hecho de que $a$ $b$ son iguales. Si $a=_Ab$ tiene un elemento, a continuación, $a$ $b$ son iguales. Desde $a=_Ab$ es un tipo, también se puede obtener un tipo de $p=_{a=_Ab}q$. Podemos repetir este proceso indefinidamente. Los diversos coherencia de las leyes de hacer esto en un $\infty$-groupoid estructura.
Un conjunto en el tipo de teoría es de un tipo tal que cualquiera de los dos elementos de un tipo de identidad son iguales. A continuación, un precategory es un tipo de objetos y, para cualquiera de los dos objetos, un tipo de conjunto de morfismos. Una categoría es un precategory donde isomorphisms de objetos son equivalentes a la igualdad. Puesto que todos los tipos tienen un $\infty$-groupoid la estructura, el tipo de objetos es una $\infty$-groupoid y también lo son todos los conjuntos de morfismos.
