4 papers
A synthetic construction of universal cocartesian fibrations
Christian Sattler, David Wärn
We give a model-independent construction of directed univalent cocartesian fibrations of -categories, and prove a straightening equivalence against such fibrations. The…
Projective Space in Synthetic Algebraic Geometry
Felix Cherubini, Thierry Coquand, Matthias Ritter +1
Synthetic algebraic geometry is a new approach to algebraic geometry. It consists in using homotopy type theory extended with three axioms, together with the interpretation of thes…
Differential Geometry of Synthetic Schemes
Felix Cherubini, Matthias Hutzler, Hugo Moeneclaey +1
Synthetic algebraic geometry uses homotopy type theory extended with three axioms to develop algebraic geometry internal to a higher version of the Zariski topos. In this article w…
Path spaces of pushouts
David Wärn
Given a span of spaces, one can form the homotopy pushout and then take the homotopy pullback of the resulting cospan. We give a concrete description of this pullback as the colimi…