On the (infinity,1)-Grothendieck construction via straightening and unstraightening entirely within the context of quasi-categories:
On the resulting interpretation of the universal coCartesian fibration as categorical semantics for a univalent type universe in directed homotopy type theory:
On the directed univalence axiom in this context:
On formal (infinity,1)-category theory:
Last revised on April 11, 2025 at 09:55:44. See the history of this page for a list of all contributions to it.