The Frobenius equivalence and Beck-Chevalley condition for Algebraic Weak Factorisation Systems

TL;DR

This paper extends the Frobenius equivalence to algebraic weak factorisation systems, providing a categorical framework that supports the construction of dependent types in type theory, with applications to groupoid models.

Contribution

It establishes an analog of the Frobenius equivalence for algebraic weak factorisation systems, enhancing their applicability in categorical semantics of type theory.

Findings

Proves Frobenius equivalence for algebraic weak factorisation systems

Demonstrates the use of split fibrations of groupoids in the framework

Provides tools for constructing dependent function types in type theory

Abstract

If a locally cartesian closed category carries a weak factorisation system, then the left maps are stable under pullback along right maps if and only if the right maps are closed under pushforward along right maps. We refer to this statement as the Frobenius equivalence and in this paper we state and prove an analogical statement for algebraic weak factorisation systems. These algebraic weak factorisation systems are an explicit variant of the more traditional weak factorisation systems in that the factorisation and the lifts are part of the structure of an algebraic weak factorisation system and are not merely required to exist. Our work has been motivated by the categorical semantics of type theory, where the Frobenius equivalence provides a useful tool for constructing dependent function types. We illustrate our ideas using split fibrations of groupoids, which are the backbone of the groupoid model of Hofmann and Streicher.