nLab autoequivalence type

 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

• $\mathrm{Aut}(A)$ is an $\infty$-group.

• Given a univalent Russell 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$.

• The autoequivalence type on an $n$-truncated type $A$ is an $(n + 1)$-group.

• If $A$ is a set, then $\mathrm{Aut}(A)$ is the symmetric group on $A$ and is also written as $S_A$, $\Sigma_A$, or $\mathrm{Sym}(A)$, and the elements of $\mathrm{Aut}(A)$ are called permutations. Every autoequivalence type is a symmetric group in a dependent type theory with axiom K or uniqueness of identity proofs.

• If $A$ is a mere proposition, then $\mathrm{Aut}(A)$ is a contractible type.

• 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

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

Examples

• There are only two autoequivalences of Cat: the identity functor and the opposite category functor. See the latter for details.

 See also

• equivalence type

• permutation, symmetric group

• automorphism group, automorphism infinity-group

• loop space type (for the equivalent for identity types)