nLab twisted arrow modality

Idea

In simplicial type theory and related approaches to synthetic (infinity,1)-category theory, the twisted arrow construction is given by a modality $(-)^\mathrm{tw}$. Unlike the twisted arrow construction in the usual analytic approaches to (infinity,1)-category theory like quasicategories or complete Segal spaces, the twisted arrow modality can be applied to any type by definition of modality, not just merely the complete Segal types.

Given a type $A$, the $n$-simplicies in $A^\mathrm{tw}$ are equivalent to the $(2n + 1)$-simplicies in $A$.

The twisted arrow modality is used in defining the (infinity,1)-Yoneda embedding.

 Related concepts

• Segal type

• Rezk type

• op modality

• twisted arrow (∞,1)-category

References

• Jonathan Weinberger, Type-theoretic modalities for synthetic $(\infty, 1)$-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)

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, The Yoneda embedding in simplicial type theory (arXiv:2501.13229)