A regular fibration is a bifibration , where and have finite products that are preserved by and that preserve cartesian arrows, satisfying Frobenius reciprocity and the Beck--Chevalley condition for pullback squares in .
The preservation conditions on products are equivalent to requiring that each fibre have finite products and that these be preserved by all reindexing funtors .
Our regular fibrations are those of Pavlovic. A very similar definition is given by Jacobs, whose only essential difference is that the fibres of a regular fibration are required to be preorders. (Hence such fibrations model regular logic where all proofs of the same sequent are considered equal.)
A regular fibration posesses exactly the structure needed to interpret regular logic?.
…
A category is regular if and only if the projection sending to is a regular fibration, where is the full subcategory of on the monomorphisms.
For our purposes, a regular category is one that has finite limits and pullback-stable images.
The ‘only if’ part of the proposition is straightforward: the adjunctions come from pullbacks and images in (Elephant lemma 1.3.1) as does the Frobenius property ( op. cit. lemma 1.3.3). The terminal object of is the identity on , and binary products in the fibres are given by pullback. The products are preserved by reindexing functors because (the are right adjoints but also because) a cone over the diagram for can be rearranged into a cone over that for , giving the two the same universal property. The projection clearly preserves these products. The Beck–Chevalley condition follows from pullback-stability of images in .
…