In simplicial type theory and bicubical type theory? and related approaches to synthetic (infinity,1)-category theory, the op modality is a modality 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 -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)
Last revised on August 9, 2024 at 14:26:03. See the history of this page for a list of all contributions to it.