A 2-categorical proof of Frobenius for fibrations defined from a generic point
arXiv:2210.00078 · doi:10.1017/S0960129524000094
Abstract
Consider a locally cartesian closed category with an object 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 I defines a trivial fibration. Then the fibrations are also closed under pushforward.
20 pages; v3 fixes some typos in the text and in couple of diagrams, it improves the introduction, and it adds new references in the bibliography. v2 adds an appendix on the constructive implications of this proof for structured fibrations