Partiality, cartesian closedness, and toposes (Q1121368)

This paper is concerned with some categorical aspects of structures with partial morphisms vis à vis to \(\lambda_ p\)-calculus of \textit{E. Moggi} [Lect. Notes Comput. Sci. 240, 242-251 (1986; Zbl 0628.03007)]. As a result of a synthesis of numerous papers published in the last decade (the papers of the authors are also included, and widely referred to in the text), the article gives a basic equational framework for categories with partial morphisms. The basic concepts are: category of partial maps (pC), lifting, partially cartesian category (pCC), domain, restriction, range, partial epi, partial mono, partial exponentiation, partially cartesian closed category (pCCC), dominion, partial topos, interval equality. In the authors' view the structure pC is an enriched (pre)-ordered category. The introduced axioms are strongly related to the intuitive concept of partiality. Notions corresponding to the ``total ones'' are defined and several basic results in pC, pCC, pCCC are established. The authors construct the category \(C_ T\) of total arrows. The main result gives conditions under which the partial properties in C imply the corresponding total properties in \(C_ T\). Using ``inverse'' constructions, the partial structures \(C_ p\) are obtained from the ``total ones'' C. Some properties of partial toposes are presented and a characterization of toposes is given: a cartesian closed category with pullbacks C is a topos iff its associated partial category \(C_ p\) is partially cartesian closed. As a final result the authors present an equational description of partial toposes and of other structures. These results have applications in the areas of programming languages and of automated categorical reasoning.