An official website of the United States government
Abstract Consider a locally cartesian closed category with an object$$\mathbb{I}$$and a class of trivial fibrations, which admit sections and are stable under pushforward and retract as arrows. Define the fibrations to be those maps whose Leibniz exponential with the generic point of$$\mathbb{I}$$defines a trivial fibration. Then the fibrations are also closed under pushforward.
more »
« less
Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher.
Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?
Some links on this page may take you to non-federal websites. Their policies may differ from this site.
-
-
Abstract Many introductions tohomotopy type theoryand theunivalence axiomgloss over the semantics of this new formal system in traditional set‐based foundations. This expository article, written as lecture notes to accompany a three‐part mini course delivered at the Logic and Higher Structures workshop at CIRM‐Luminy, attempt to survey the state of the art, first presenting Voevodsky's simplicial model of univalent foundations and then touring Shulman's vast generalization, which provides an interpretation of homotopy type theory with strict univalent universes in any ‐topos. As we will explain, this achievement was the product of a community effort to abstract and streamline the original arguments as well as develop new lines of reasoning.more » « less
-
Forster, Yannick; Keller, Chantal (Ed.){"Abstract":["Certain results involving "higher structures" are not currently accessible to computer formalization because the prerequisite ∞-category theory has not been formalized. To support future work on formalizing ∞-category theory in Lean’s mathematics library, we formalize some fundamental constructions involving the 1-category of categories. Specifically, we construct the left adjoint to the nerve embedding of categories into simplicial sets, defining the homotopy category functor. We prove further that this adjunction is reflective, which allows us to conclude that 𝒞at has colimits. To our knowledge this is the first formalized proof that the nerve functor is a fully faithful right adjoint and that the category of categories is cocomplete."]}more » « lessFree, publicly-accessible full text available September 22, 2026
