# nLab bi-invertible morphism

### Context

#### Higher category theory

higher category theory

# Contents

## Idea

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.

## Definition

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

## Examples

An integers object in an (n,1)-category $C$ with a terminal object is defined as the (homotopy) initial object $\mathbb{Z}$ with a global element $0:Mor(1, \mathbb{Z})$ and a bi-invertible endomorphism $\mathrm{succ}:Mor(\mathbb{Z}, \mathbb{Z})$ with section $\mathrm{pred}_1:Mor(\mathbb{Z}, \mathbb{Z})$ and retraction $\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.