nLab op modality

Contents

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(-)^\op which takes a Segal type, representing (infinity,1)-precategories, and turns it into the opposite Segal type, representing the opposite (infinity,1)-precategory.

References

Last revised on August 9, 2024 at 14:26:03. See the history of this page for a list of all contributions to it.