Finn Lawler regular fibration (Rev #1)

Contents

Definition

A regular fibration is a bifibration p:EBp \colon E \to B, where EE and BB have finite products, with those in EE preserved by reindexing (f *A×f *Bf *(A×B)f^*A \times f^*B \cong f^*(A \times B)), satisfying Frobenius reciprocity and the Beck--Chevalley condition for pullback squares in BB.

Logic

A regular fibration posesses exactly the structure needed to interpret regular logic?.

Characterization

Proposition

A category CC is regular if and only if the projection cod:Mon(C)Ccod \colon Mon(C) \to C sending SXS \hookrightarrow X to XX is a regular fibration, where Mon(C)Mon(C) is the full subcategory of C C^{\to} on the monomorphisms.

Proof

Revision on February 1, 2011 at 18:30:01 by Finn Lawler?. See the history of this page for a list of all contributions to it.