Verallgemeinerte Chevalley-Kriterien in simplizialem Homotopie-Typentheorie

Wir stellen eine verallgemeinerte Behandlung von (ko)kartesischen Pfeilen, Faserbündeln und Funktoren bereit. Im Vergleich zu den klassischen Bedingungen werden die Endpunkteinbettungen durch beliebige Formeinbettungen ersetzt. Unser Rahmen ist die simpliziale Homotopie-Typentheorie von Riehl-Shulman, die die Entwicklung einer synthetischen internen (∞, 1)-Kategorientheorie unterstützt.