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

TL;DR

This paper provides a 2-categorical proof demonstrating that fibrations, defined via Leibniz exponential with a generic point in a locally cartesian closed category, are closed under pushforward, extending Frobenius properties.

Contribution

It introduces a 2-categorical proof of Frobenius for fibrations defined from a generic point in a locally cartesian closed category.

Findings

Fibrations are closed under pushforward.

Fibrations admit sections and are stable under retracts.

The proof extends Frobenius properties in a 2-categorical setting.

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.