nLab isomorphism in a Segal type



In simplicial type theory, given a Segal type AA and terms x:Ax \colon A and y:Ay \colon A, a “morphism” (term of hom type) f:hom A(x,y)f \colon \mathrm{hom}_A(x, y) is an isomorphism if there exist morphisms g:hom A(y,x)g:\mathrm{hom}_A(y, x) and h:hom A(y,x)h:\mathrm{hom}_A(y, x) such that gf=id xg \circ f = \mathrm{id}_x and fh=id yf \circ h = \mathrm{id}_y

isIso(f)( g:hom A(y,x)gf=id x)×( h:hom A(y,x)fh=id y)\mathrm{isIso}(f) \coloneqq \left(\sum_{g:\mathrm{hom}_A(y, x)} g \circ f = \mathrm{id}_x\right) \times \left(\sum_{h:\mathrm{hom}_A(y, x)} f \circ h = \mathrm{id}_y\right)

The type of all isomorphisms between xx and yy in AA is defined as

(x Ay) f:hom A(x,y)isIso(f) \big(x \cong_A y\big) \;\;\coloneqq\;\; \sum_{ \mathclap{ f \colon \mathrm{hom}_A(x, y) } } \mathrm{isIso}(f)


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