A paper on categorical proof theory MAPS II: CHASING PROOFS IN THE LAMBEK-LAWVERE LOGIC by Dusko Pavlovic is available by anonymous FTP from triples.math.mcgill.ca. The file is called mapsII, and there are -A4 and -US formats, in .dvi and .ps files. Please let me know if you have any problems with these files. -- Regards, Dusko Abstract In the Lambek-Lawvere logic, propositions and proofs are presented as objects and arrows in a category. It is the categorical embodiment of the strong constructivist paradigms of propositions-as-types and proofs-as-constructions, which lie in the foundation of computational logic. But a third paradigm arises here, not available elsewhere: the idea of logical-operations-as-adjunctions. It opens a possibility of genuinely categorical proof theory. In the present paper, we study the Lambek-Lawvere version of regular logic: the $\{\wedge,\exists\}$-fragment of the first order logic with equality. The corresponding categorical structure is regular fibration. The examples include stable factorisations, sites, triposes. Regular logic is exactly what is needed to talk about maps, as total and single-valued relations. However, when enriched with proofs-as-arrows, this familiar concept must be supplied with an additional conversion rule, connecting the proof of the totality with the proof of the single-valuedness. We explain the logical meaning of this and describe conditions under which every map in a regular fibration corresponds to a unique arrow in the base category. When this is the case, a natural fragment of generalized regular logic, in the Lambek-Lawvere style, reduces to regular logic of sites. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++