A characterisation of elementary fibrations (Q2131276)

This article provides several characterizations of what the authors name ``elementary'' fibrations. These are intended to be those fibrations which also support a structure of equality. Following Lawvere's program, the idea is that such a structure should be expressed by adjunction. The proposed definition of elementary fibration requires certain adjunctions in fibres plus conditions, namely Frobenius Reciprocity and Beck-Chevalley -- the latter usually indicating an indexed adjunction. The equivalents to the condition of being an elementary fibration are mostly rather technical. Some useful examples are provided and moreover the characterizations are used to explore relationships with algebraic weak factorization systems and also with the Hofmann-Streicher groupoid model of Martin-Löf Type Theory.