In dependent type theory, given a type$A$, the autoequivalence type of $A$ is the equivalence type between $A$ and $A$ itself, $\mathrm{Aut}(A) \coloneqq (A \simeq A)$. The elements (terms) of $\mathrm{Aut}(A)$ are called autoequivalences or self-equivalences.

Given a univalentRussell universe$U$ and an element $A:U$, there is an equivalence between $\mathrm{Aut}(A)$ and the loop space type$\Omega(U, A)$, $\mathrm{ua}(A, A):\Omega(U, A) \simeq \mathrm{Aut}(A)$. $\Omega(U, A)$ is called the automorphism $\infty$-group in $U$ at $A$.

Given types $A$ and $B$, there is a function$\mathrm{ae}_\mathrm{Aut}:(A \simeq B) \to (\mathrm{Aut}(A) \simeq \mathrm{Aut}(B))$.

Deloopings

Given an infinity-group$A$, the delooping of $A$ is defined to be a higher inductive type$B(A)$ generated by equivalences $\delta_A:\mathrm{Aut}(B(A)) \simeq A$ and $\epsilon_A:B(\mathrm{Aut}(A)) \simeq A$, and identity