Contents

Definition

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.

Properties

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

$\kappa_A:\mathrm{ae}_\mathrm{Aut}(\epsilon_A) =_{\mathrm{Aut}(B(\mathrm{Aut}(A))) \simeq \mathrm{Aut}(A)} \delta_{\mathrm{Aut}(A)}$