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…
The algebraic small object argument as a saturation
Evan Cavallo, Christian Sattler
We analyze the structure of left maps in algebraic weak factorization systems constructed using Garner's algebraic small object argument. We find that any left map can be construct…
Free monad sequences and extension operations
Christian Sattler
In the first part of this article, we give an analysis of the free monad sequence in non-cocomplete categories, with the needed colimits explicitly parametrized. This enables us to…
Natural numbers from integers
Christian Sattler, David Wärn
In homotopy type theory, a natural number type is freely generated by an element and an endomorphism. Similarly, an integer type is freely generated by an element and an automorphi…