nLab opposite simplicial infinity-groupoid

Definition

For $A$ a simplicial $\infty$-groupoid, its opposite is the simplicial $\infty$-groupoid $A^{op}$ obtained by reversing the order of all the face and degeneracy maps.

Properties

The operation extends to an automorphic $(\infty,1)$-functor

$$(-)^\op : \infty\mathrm{Grpd}^{\Delta^\op} \to \infty\mathrm{Grpd}^{\Delta^\op}$$

from SimpInfGrpd to itself. When the op $(\infty,1)$-functor is restricted to the $(\infty,1)$-subcategory $(\infty,1)\mathrm{Cat} \hookrightarrow \infty\mathrm{Grpd}^{\Delta^\op}$, it takes $(\infty,1)$-categories to its opposite $(\infty,1)$-category.

In simplicial type theory thought of as the internal logic of $\infty\mathrm{Grpd}^{\Delta^\op}$, the opposite simplicial $\infty$-groupoid is given by the op modality.

Related concepts

• simplicial infinity-groupoid

• opposite (infinity,1)-category

• op modality