Primero lo primero: su observación es esencialmente el hecho de que $\mathbf{Iso}(\mathcal{C})$ es un objeto de trazado para $\mathcal{C}$. Más precisamente, se observa que para cualquier categoría de $\mathcal{C}$, tenemos una factorización
$$\mathcal{C} \to \mathbf{Iso}(\mathcal{C}) \to \mathcal{C} \times \mathcal{C}$$
de la diagonal functor $\Delta : \mathcal{C} \to \mathcal{C} \times \mathcal{C}$ donde $\mathbf{Iso}(\mathcal{C}) \to \mathcal{C} \times \mathcal{C}$ es un isofibration y $\mathcal{C} \to \mathbf{Iso}(\mathcal{C})$ es inyectiva en objetos de equivalencia, así que de hecho tienen un objeto de trazado en el sentido de categorías de modelo. En particular, las fibras de $\mathbf{Iso}(\mathcal{C}) \to \mathcal{C} \times \mathcal{C}$ parametrise caminos entre los "puntos" (es decir, objetos) en $\mathcal{C}$, como uno espera.
Por otro lado, la univalence axioma dice que hay una clasificación de espacio para los tipos en los que el espacio de las rutas entre dos puntos cualesquiera es canónicamente equivalente al espacio de correspondencias entre los tipos correspondientes. Es evidente que existe una generalización de este si reemplazamos "tipo" con el "objeto en una categoría", y que conduce a Rezk la noción de integridad.
Por lo tanto, con el fin de hacer una conexión entre el $\mathbf{Iso}(\mathcal{C})$ y univalence, necesitamos una noción de la clasificación de espacio para los objetos en $\mathcal{C}$. Hay varios candidatos:
- El conjunto $\operatorname{ob} \mathcal{C}$.
- El nervio de la $\operatorname{iso} \mathcal{C}$, la máxima subgroupoid de $\mathcal{C}$.
- El nervio de la $\mathcal{C}$ sí.
Obviamente, $\operatorname{ob} \mathcal{C}$ no trabajo en general. Menos obviamente, el nervio de la $\mathcal{C}$ no trabajo en general. Pero el nervio de $\operatorname{iso} \mathcal{C}$ tiene la propiedad requerida, más o menos, por definición.
De alguna manera, la de arriba no es muy interesante, porque hemos construido la clasificación de espacio para que el "univalence" axioma es satisfecho. Es mucho más interesante pensar acerca de la situación general en donde la clasificación de espacio es "built-in".
Deje $\mathcal{S}$ ser un buen categoría de "espacios", por ejemplo, simplicial conjuntos, o incluso groupoids. Un precategory o Segal objeto en $\mathcal{S}$ es un objeto simplicial $X_{\bullet}$ la satisfacción de las Segal condición:
- Para todos los $n \ge 2$, la canónica de morfismos
$$X_n \to \mathrm{ho}{\varprojlim} \left( X_0 \leftarrow X_1 \rightarrow X_0 \leftarrow \cdots \rightarrow X_0 \leftarrow X_1 \rightarrow X_0 \right)$$
es un débil equivalencia en $\mathcal{S}$.
En el caso de que $X_0$ es discreto, se puede sustituir $\mathrm{ho}{\varprojlim}$$\varprojlim$. Existe una noción de equivalencia de precategories, pero estos no tienen que inducir débil de equivalencias de la $0$-th espacios – así que, en cierto sentido, el $0$-th espacio es indeterminado.
Existe una noción de equivalencia en un precategory $X_{\bullet}$, y esto determina un subespacio $X_\mathrm{eq} \subseteq X_1$ que consta de los componentes conectados, cuyos puntos son equivalencias. Por supuesto, la degeneración operador $X_0 \to X_1$ factores a través de $X_\mathrm{eq}$. Una categoría o completa Segal objeto en $\mathcal{S}$ es un precategory $X_{\bullet}$ que satisface Rezk integridad del axioma:
- La canónica de morfismos $X_0 \to X_\mathrm{eq}$ es un débil equivalencia en $\mathcal{S}$.
Rezk-integridad tiene las siguientes agradable consecuencia: una de morfismos de categorías es una equivalencia de precategories si y sólo si es un degreewise débil de equivalencia. Por otra parte, como el nombre sugiere, cada precategory admite un Rezk finalización, es decir, es equivalente a una categoría.
Finalmente, se puede atar de nuevo el univalence: el univalence axioma puede ser interpretado como decir que la precategory de tipos es Rezk-completa. Esto es muy conveniente, porque Rezk-integridad es conservado por muchos construcciones.
Adenda. Sorprendentemente, la definición de Rezk-categorías completas en $\mathbf{Grpd}$ ya estaba más o menos presentes en [Hofmann y Streicher, El groupoid interpretación de la teoría tipo, §5.5], todo el camino de regreso en 1996! Por comparación, [Rezk, Un modelo para la homotopy teoría de homotopy teoría] apareció en arXiv sólo en 1998.
