nLab discrete Segal type



In simplicial type theory, a Segal type AA is a discrete Segal type if for all elements x:Ax:A and y:Ay:A there is an equivalence between the identity type x= Ayx =_A y and the hom type hom A(x,y)\mathrm{hom}_A(x, y):

x:A,y:Adisc(x,y):isEquiv(idToHom(x,y))x:A, y:A \vdash \mathrm{disc}(x, y):\mathrm{isEquiv}(\mathrm{idToHom}(x, y))


idToHom(x,y):(x= Ay)hom A(x,y) \mathrm{idToHom}(x, y) \;\colon\; (x =_A y) \; \to \; \mathrm{hom}_A(x, y)
idToHom(x,y)(refl A(x))id A(x) \mathrm{idToHom}(x, y) \big( \mathrm{refl}_A(x) \big) \;\coloneqq\; \mathrm{id}_A(x)


Created on May 21, 2023 at 13:27:16. See the history of this page for a list of all contributions to it.