nLab Segal type

Contents

 Idea

Segal types are the (infinity,1)-categorical version of precategories in simplicial type theory

Definition

In simplicial type theory, a Segal type is a type AA such that given elements x:Ax:A, y:Ay:A, and z:Az:A and morphisms f:hom A(x,y)f:\mathrm{hom}_A(x, y) and g:hom A(y,z)g:\mathrm{hom}_A(y, z), the type

h:hom A(x,z)Δ 2A| [x,y,z,f,g,h] Δ 2\sum_{h:\mathrm{hom}_A(x, z)} \left\langle \Delta^2 \to A \vert_{[x, y, z, f, g, h]}^{\partial \Delta^2} \right\rangle

is a contractible type, where Δ 2\Delta^2 is the 22-simplex probe shape and Δ 2\partial \Delta^2 is its boundary.

References

Last revised on January 1, 2024 at 01:55:22. See the history of this page for a list of all contributions to it.