nLab isomorphism in simplicial type theory

Definition

There are many possible definitions of an isomorphism in simplicial type theory.

Bi-invertible morphisms

In simplicial type theory, given a type $A$ and terms $x:A$ and $y:A$, a morphism $f:\mathrm{hom}_A(x, y)$ is a bi-invertible morphism if the span $(f, \mathrm{id}_x)$ has a left quotient and the cospan $(\mathrm{id}_y, f)$ has a right quotient.

$$\mathrm{isIso}(f) \coloneqq \mathrm{leftQuotient}(f, \mathrm{id}_x) \times \mathrm{rightQuotient}(\mathrm{id}_y, f)$$

Merely quasi-invertible morphisms

In simplicial type theory, given a type $A$ and terms $x:A$ and $y:A$, a morphism $f:\mathrm{hom}_A(x, y)$ is a quasi-invertible morphism if one can construct a morphism $g:\mathrm{hom}_A(y, x)$ called a quasi-inverse such that $\mathrm{id}_x$ is the unique composite of $f$ and $g$ and $\mathrm{id}_y$ is the unique composite of $g$ and $f$.

$$\mathrm{quasiInverses}(f) \coloneqq \sum_{g:\mathrm{hom}_A(y, x)} \mathrm{isUniqueComposite}(f, g, \mathrm{id}_x) \times \mathrm{isUniqueComposite}(g, f, \mathrm{id}_y)$$

A morphism $f:\mathrm{hom}_A(x, y)$ is a merely quasi-invertible morphism if there merely exists $g:\mathrm{hom}_A(y, x)$ such that $\mathrm{id}_x$ is the unique composite of $f$ and $g$ and $\mathrm{id}_y$ is the unique composite of $g$ and $f$.

$$\mathrm{isIso}(f) \coloneqq \exists g:\mathrm{hom}_A(y, x).\mathrm{isUniqueComposite}(f, g, \mathrm{id}_x) \times \mathrm{isUniqueComposite}(g, f, \mathrm{id}_y)$$

If $A$ is a Segal type, this is equivalent to the usual definition of a merely quasi-invertible morphism

$$\mathrm{isIso}(f) \coloneqq \exists g:\mathrm{hom}_A(y, x).(g \circ f = \mathrm{id}_x) \times (f \circ g = \mathrm{id}_y)$$

Equivalence of definitions

These definitions of an isomorphism are equivalent for Segal types. It is unknown whether the definitions are still equivalent for types which are not Segal, and if not, which notion of isomorphism is the right notion for non-Segal types.

Type of isomorphisms

The type of isomorphisms is given by the dependent sum type

$$\mathrm{iso}_A(x, y) \coloneqq \sum_{:\mathrm{hom}_A(x, y)} \mathrm{isIso}(f)$$

We say that two elements $x:A$ and $y:A$ are merely isomorphic if there merely exists an isomorphism between $x$ and $y$:

$$x \cong_A y \coloneqq \exists f:\mathrm{hom}_A(x, y).\mathrm{isIso}(f)$$

Related concepts

• hom type

• univalent type

• Rezk type

• skeletal type

• isomorphism

• equivalence in an (∞,1)-category

• span in simplicial type theory

• cospan in simplicial type theory

References

• Emily Riehl, Michael Shulman, A type theory for synthetic $\infty$-categories $[$arXiv:1705.07442$]$

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)