- homotopy hypothesis-theorem
- delooping hypothesis-theorem
- periodic table
- stabilization hypothesis-theorem
- exactness hypothesis
- holographic principle

- (n,r)-category
- Theta-space
- ∞-category/∞-category
- (∞,n)-category
- (∞,2)-category
- (∞,1)-category
- (∞,0)-category/∞-groupoid
- n-category = (n,n)-category
- n-poset = (n-1,n)-category
- n-groupoid = (n,0)-category

- categorification/decategorification
- geometric definition of higher category
- algebraic definition of higher category
- stable 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**

**Introductions**

**Definitions**

**Paths and cylinders**

**Homotopy groups**

**Basic facts**

**Theorems**

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)$ 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.

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.

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

- Thorsten Altenkirch, Luis Scoccola,
*The Integers as a Higher Inductive Type*, arXiv

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