\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{regular fibration}

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{the_typea_beckchevalley_condition}{The type-A Beck--Chevalley condition}\dotfill \pageref*{the_typea_beckchevalley_condition} \linebreak
\noindent\hyperlink{logic}{Logic}\dotfill \pageref*{logic} \linebreak
\noindent\hyperlink{characterization}{Characterization}\dotfill \pageref*{characterization} \linebreak


\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

A \textbf{pre-regular fibration} is a [[nlab:bifibration]] $p \colon E \to B$, where $E$ and $B$ have finite products that are preserved by $p$ and that preserve cartesian arrows, satisfying [[nlab:Frobenius reciprocity]] and the [[nlab:Beck--Chevalley condition]] for [[product-absolute pullback]] squares of \textbf{types C}, \textbf{D} and \textbf{E} in $B$. A \textbf{regular fibration} is a pre-regular fibration that also satisfies the Beck--Chevalley condition for \textbf{type-B} squares.

The preservation conditions on products are equivalent to requiring that each fibre $E_A$ have finite products and that these be preserved by all reindexing functors $f^*$.

\hypertarget{the_typea_beckchevalley_condition}{}\subsubsection*{{The type-A Beck--Chevalley condition}}\label{the_typea_beckchevalley_condition}

Here and in my thesis I originally required regular fibrations to satisfy the type-A BC condition, but I now believe that it holds automatically as long as E does.

By \href{References#shulman08framed}{Shulman's construction}, a pre-regular fibration $E$ over $B$ gives rise to a cartesian equipment $B \to Matr(E)$, and hence a cartesian bicategory $Matr(E)$. Type-E squares in the bicategory are exact because they satisfy the BC condition in the fibration. $Matr(E)$ then becomes compact closed bicategory, which is to say that there is an equivalence $hom(A \times B, C) \simeq hom(A, C \times B)$ given by composing with $A \times d_\bullet e^\bullet$ (left to right) and with $C \times d^\bullet e_\bullet$ (right to left), where $d$ is the diagonal at $B$ and $e$ the map from $B$ to the terminal object. We will write this as $R^\wedge \colon A \to C \times B$ for $R \colon A \times B \to C$ and $S^\vee \colon A \times B \to C$ for $S \colon A \to C \times B$. Similarly there is an equivalence $hom(A \times B, C) \simeq hom(B, A \times C)$, which we will write as ${}^\wedge T$ and ${}^\vee U$. If $R \colon A \to B$ then $R^\circ = {}^\vee (R^\wedge) \cong {}^\wedge (R^\vee)$. The type-E BC condition implies that $f_\bullet \dashv f_\bullet^\circ$, and therefore $f_\bullet^\circ \cong f^\bullet$, and also that $d_\bullet^\vee \cong d^\bullet$ and $(d^\bullet)^\wedge \cong d_\bullet$. (See \href{References#cw87cartesian}{Carboni--Walters} and \href{References#ww08frobenius}{Walters--Wood} for all of this.)

The claim now is that modulo these isomorphisms, the morphisms required to be invertible by exactness of or BC for type-A squares are equal to $\beta_1 = (d_\bullet f_\bullet \cong (f \times f)_\bullet d_\bullet)^\vee$ and $\beta_2 = {}^\wedge \beta_1$. Being the images under equivalences of invertible morphisms, then, they must themselves be invertible.

The following pictures show the essential parts of the proof using string diagrams, which can be read top-to-bottom as morphisms in a cartesian bicategory or bottom-to-top as objects in a monoidal bifibration as in \href{http://www.tac.mta.ca/tac/volumes/26/23/26-23abs.html}{this paper}.

\begin{itemize}%
\item \href{/finnlawler/files/bc-1.jpg}{Page 1}
\item \href{/finnlawler/files/bc-2.jpg}{Page 2}
\item \href{/finnlawler/files/bc-3.jpg}{Page 3}
\item \href{/finnlawler/files/bc-4r.jpg}{Page 4}
\item \href{/finnlawler/files/bc-5r.jpg}{Page 5}

\end{itemize}
\hypertarget{logic}{}\subsection*{{Logic}}\label{logic}

A regular fibration posesses exactly the structure needed to interpret regular logic, i.e. the ${\exists}{\wedge}{\top}$-fragment of first-order logic.

\ldots{}

\hypertarget{characterization}{}\subsection*{{Characterization}}\label{characterization}

\begin{prop}
\label{}\hypertarget{}{}
A category $C$ is [[nlab:regular category|regular]] if and only if the subobject fibration $Sub(C) \to C$ (that sends $S \hookrightarrow X$ to $X$) is regular.

\end{prop}
\begin{proof}
For our purposes, a regular category is one that has [[nlab:finite limits]] and [[nlab:pullback]]-stable [[nlab:image|images]].

If $C$ is a regular category, then the adjunctions $\exists_f \dashv f^*$ come from pullbacks and images in $C$ (\href{References#elephant}{Elephant} lemma 1.3.1) as does the Frobenius property (${}$\emph{op. cit.} lemma 1.3.3). The terminal object of $Sub(A) = Sub(C)_A$ is the identity $1_A$ on $A$, and binary products in the fibres $Sub(A)$ are given by pullback. The products are preserved by reindexing functors $f^*$ because (the $f^*$ are right adjoints but also because) $f^*(S \wedge S')$ and $f^*S \wedge f^*S'$ have the same universal property. The projection $Sub(C) \to C$ clearly preserves these products. The Beck--Chevalley condition follows from pullback-stability of images in $C$.

Conversely, suppose $Sub(C) \to C$ is a regular fibration. We need to show that $C$ has equalizers (to get finite limits) and pullback-stable images. But the equalizer of $f, g \colon A \rightrightarrows B$ is $(f,g)^*\Delta$. For images, let $im f = \exists_f 1$ as in \href{References#elephant}{Elephant} lemma 1.3.1. Pullback-stability follows from the Beck--Chevalley condition, which holds for all pullback squares in $C$ by \href{References#seely83hyper}{Seely}, Theorem sec. 8.

\end{proof}
[[!redirects regular fibrations]]



\end{document}