nLab Rezk type



In simplicial type theory, a Segal type AA is a Rezk 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 type of isomorphisms in a Segal type x Ayx \cong_A y:

x:A,y:ARezkComplete(x,y):isEquiv(idToIso(x,y))x:A, y:A \vdash \mathrm{RezkComplete}(x, y):\mathrm{isEquiv}(\mathrm{idToIso}(x, y))


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


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