nLab op modality



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.


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