nLab op modality

Idea

In simplicial type theory and related approaches to synthetic simplicial anima, the op modality is a modality $(-)^\op$ which takes a type, representing simplicial anima, and turns it into the opposite type, representing the opposite simplicial anima.

In particular, for (infinity,1)-category theory, the modality can take a complete Segal type, representing (infinity,1)-categories, and turns it into the opposite complete Segal type, representing the opposite (infinity,1)-category.

 Related concepts

• opposite simplicial infinity-groupoid

• simplicial type theory

• twisted arrows modality

References

• Jonathan Weinberger, Type-theoretic modalities for synthetic $(\infty, 1)$-categories, Talk at Homotopy Type Theory 2019, August 14, 2019. (slides)

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, The Yoneda embedding in simplicial type theory (arXiv:2501.13229)