nLab op modality

Idea

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.

 Related concepts

• Segal type

• Rezk type

References

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