In simplicial type theory and bicubical type theory? and related approaches to synthetic (infinity,1)-category theory, the **op modality** is a modality $(-)^\op$ which takes a Segal type, representing (infinity,1)-precategories, and turns it into the opposite Segal type, representing the opposite (infinity,1)-precategory.

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

Created on September 19, 2023 at 14:44:45. See the history of this page for a list of all contributions to it.