A 2-categorical proof of Frobenius for fibrations defined from a generic point

Link to journal publication

arXiv Preprint

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. 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.