nLab bi-invertible morphism


Higher category theory

higher category theory

Basic concepts

Basic theorems





Universal constructions

Extra properties and structure

1-categorical presentations

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts




In (n,1)-categories and (infinity,1)-categories, the usual definition of invertible morphism is too strict and would violate the principle of equivalence. There are a few options to resolve this issue: one is by using weak inverses; but another is by using bi-invertible morphisms, which are a generalization of the notion of bi-invertible function in type theory.


A morphism f:Mor(A,B)f:Mor(A, B) in a (n,1)-category or (infinity,1)-category is bi-invertible if there are morphisms sec(f):Mor(B,A)\mathrm{sec}(f):Mor(B, A) and ret(f):Mor(B,A)\mathrm{ret}(f):Mor(B, A) such that sec(f)\mathrm{sec}(f) is a section of ff and ret(f)\mathrm{ret}(f) is a retraction of ff, with section and retraction defined using path space objects rather than strict equality.


An integers object in an (n,1)-category CC with a terminal object is defined as the (homotopy) initial object \mathbb{Z} with a global element 0:Mor(1,)0:Mor(1, \mathbb{Z}) and a bi-invertible endomorphism succ:Mor(,)\mathrm{succ}:Mor(\mathbb{Z}, \mathbb{Z}) with section pred 1:Mor(,)\mathrm{pred}_1:Mor(\mathbb{Z}, \mathbb{Z}) and retraction pred 2:Mor(,)\mathrm{pred}_2:Mor(\mathbb{Z}, \mathbb{Z}). This corresponds to a definition of the integers higher inductive type in the internal logic of an (n,1)-category.

See also


For the integers object as defined with a bi-invertible morphism in the internal logic of a (infinity,1)-category see

Last revised on November 1, 2022 at 12:53:02. See the history of this page for a list of all contributions to it.