Abstract This paper responds to Rosolini’s suggestion to use the ultracompletion of a category as a way to understand versions of conceptual completeness. Over 50 years ago, Kock and Mikkelsen observed in effect that one obtains ultracompletions of the category of sets by factorising ultrapower functors. They gave a concrete description of the factorisation under what they recognised were special conditions. In parallel work, Volger obtained a different description using categorical logic. Here, I revisit these ideas using Tripos Theory and show in particular that any left exact functor of toposes admits a Kock–Mikkelsen factorisation. In this reading, the ultracompletion appears amongst the various regular and exact completions which have been studied in particular by members of the Italian Category Theory School.

Recent developments in the categorical foundations of universal algebra have given an impetus to an understanding of the lambda calculus coming from categorical logic: an interpretation is a semi-closed algebraic theory. Scott's representation theorem is then completely natural and leads to a precise Fundamental Theorem showing the essential equivalence between the categorical and more familiar notions.

One natural way to generalise domain theory is to replace partially ordered sets by categories. This kind of generalisation has recently found application in the study of concurrency. An outline is given of the elegant mathematical foundations that have been developed. This is specialised to give a construction of cartesian closed categories of domains, which throws light on standard presentations of domain theory.

We show how to construct the category of games and innocent strategies from a more primitive category of games. On that category we define a comonad and monad with the former distributing over the latter. Innocent strategies are the maps in the induced two-sided Kleisli category. Thus the problematic composition of innocent strategies reflects the use of the distributive law. The composition of simple strategies, and the combinatorics of pointers used to give the comonad and monad are themselves described in categorical terms. The notions of view and of legal play arise naturally in the explanation of the distributivity. The category-theoretic perspective provides a clear discipline for the necessary combinatorics.

We address the question of how elegantly to combine a number of different structures, such as finite product structure, monoidal structure, and colimiting structure, on a category. Extending work of Marmolejo and Lack, we develop the definition of a pseudo-distributive law between pseudo-monads, and we show how the definition and the main theorems about it may be used to model several such structures simultaneously. Specifically, we address the relationship between pseudo-distributive laws and the lifting of one pseudo-monad to the 2-category of algebras and to the Kleisli bicategory of another. This, for instance, sheds light on the preservation of some structures but not others along the Yoneda embedding. Our leading examples are given by the use of open maps to model bisimulation and by the logic of bunched implications.

We present a new category of games on graphs and derive from it a model for Intuitionistic Linear Logic. Our category has the computational flavour of concrete data structures but embeds fully and faithfully in an abstract games model. It differs markedly from the usual Intuitionistic Linear Logic setting for sequential algorithms. However, we show that with a natural exponential we obtain a model for PCF essentially equivalent to the sequential algorithms model. We briefly consider a more extensional setting and the prospects for a better understanding of the Longley Conjecture.

Realizability and related functional interpretations provide models for constructive mathematics. Generally, these models do not validate the axiom of choice for propositions taken over hierarchies of extensional functionals. We describe simple classes of models where the axiom is validated.

Article Symmetric monoidal sketches Share on Authors: Martin Hyland Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, Mill Lane, Cambridge CB2 1SB, England Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, Mill Lane, Cambridge CB2 1SB, EnglandView Profile , John Power Laboratory for the Foundations of Computer Science, University of Edinburgh, King's Buildings, Edinburgh EH9 3JZ, Scotland Laboratory for the Foundations of Computer Science, University of Edinburgh, King's Buildings, Edinburgh EH9 3JZ, ScotlandView Profile Authors Info & Claims PPDP '00: Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programmingSeptember 2000 Pages 280–288https://doi.org/10.1145/351268.351299Online:01 September 2000Publication History 7citation298DownloadsMetricsTotal Citations7Total Downloads298Last 12 Months5Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access