nLab Segal type



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


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(x,y)g:\mathrm{hom}_A(x, y), 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.


Last revised on September 19, 2023 at 14:36:52. See the history of this page for a list of all contributions to it.