A regular fibration is a bifibration , where and have finite products preserved by , satisfying Frobenius reciprocity and the Beck--Chevalley condition for pullback squares in .
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.
…