Synthetic fibered $(\infty ,1)$-category theory

Abstract

We study cocartesian fibrations in the setting of the synthetic $(\infty ,1)$-category theory developed in the simplicial type theory introduced by Riehl and Shulman. Our development culminates in a Yoneda Lemma for cocartesian fibrations.

92 pages, comments welcome; v6: final version

References in corpus (4)

• Higher Topos Theory
• All $(\infty ,1)$-toposes have strict univalent universes
• The stack of higher internal categories and stacks of iterated spans
• Classifying Types

Cited by in corpus (1)

• Yoneda Lemma for $\mathcal{D}$-Simplicial Spaces