Nearly Representable Monads and Artin Glueing The free monoid monad F has the following three properties: 1) Preserves connected limits 2) The extension of F to the product completion of Sets is representable 3) The Artin Glueing of F is a presheaf topos. In a recent paper with P.T. Johnstone (`Connected limits, familial representability and Artin glueing', to appear in Proceedings of CTCS-5 (Amsterdam, 1993), Math. Structures in Comp. Sci.) we show that in fact all the three properties are equivalent for a functor F:P --> Set, when P is a presheaf category, and more generally, that 1) and 3) are equivalent conditions when also the codomain is a presheaf category. When F is the functor part of a monad for which unit and multiplication are cartesian, then we also provide a syntactic characterization of the previous equivalent conditions ("strong regularity"), and we show that the conditions on the unit and multiplication can not be omitted. The same class of monads also appeared in a recent paper of G.M. Kelly, where they were characterized as the clubs over the free monoid monad in the category of Sets. In proving that 3) implies 1), we develop a general technique for reflecting categorical properties of the glueing to properties of the functor; for example, we show that cartesian closedness of the glueing is already sufficient to imply that the functor takes products to pullbacks over F(1), and that local cartesian closedness implies that the functor preserves pullbacks.
Some remarks on hybrid systems An important part of concurrency, the study of systems with many activities occurring together, is the study of hybrid dynamical systems. Hybrid systems are dynamical systems with two levels of description. On the one hand they are continuous systems whose behaviour is governed by differential equations. But they also have an internal structure allowing them to be viewed as discrete machines -- they undergo discrete activities passing through discrete states. The change from one discrete state to another occurs over an interval of time which may be state-dependent, and hence successive discrete actions cannot be identified with regular interval of time. A simple example is a heating system with a temperature controller. The continuous activity is the heating and cooling; the discrete activity is the switching on and off of the thermostat. Asynchronous circuits provide another class of examples of particular interest in this talk. Several automata models have been proposed for analysing hybrid systems. The aim of this lecture, reporting joint work with Piergiulio Katis (Sydney) and Nicoletta Sabadini (Milano), is to give a precise definition of such systems, to provide a calculus for constructing and analysing them using a structured kind of automata called distributive automata -- automata constructed using the operations of a distributive category -- and to prove a sheaf representation theorem for distributive automata which makes the spatial distribution of state explicit. We relate our work with the event logic of asynchronous circuits. Notice that this work is not the analytic study of the observation of instantaneous events in continuous systems as some models of concurrency appear to be. It is instead the study of continuous systems tempered to behave in a discrete way, and their use in synthesizing hybrid machines.
Aspects of cosheaves The notion of a cosheaf on a topological space is given by duality from that of a sheaf. It appears in the Borel-Moore Homology theory obtained by duality from sheaf cohomology (1960). The covering space equivalent to the notion of a cosheaf is discussed implicitly by R.H.Fox (1957) in his theory of covering spaces with singularities. A comparison between the two versions of cosheaves is given by G. Bergman (1991) for complete metric spaces and extended by J. Funk (1993) for arbitrary locales. In my paper "Cosheaves and Distributions on Toposes" (to appear in the A.Day issue of Algebra Universalis) it is shown that Lawvere distributions on a topos are cosheaves on a site of definition. Thus, results about distributions are useful in order to understand cosheaves and vuiceversa. The following are proved Theorem 1. The forgetful 2- functor from the 2-category of bounded S-toposes to the 2-category of cocomplete (small presented) S-indexed categories has a left 2-adjoint. Corollaries are: (1) the existence of the symmetric topos of a topos; (2) calculation of limits of toposes and geometric morphisms as colimits of cocomplete underlying S-indexed categories and inverse image parts of geometric morphisms; (3) the theory of S-valued cosheaves on a site is coherent. Theorem 2. (Structure of cosheaves). For any given site, the category of cosheaves on the site is equivalent to a category of G-cosheaves for a localic groupoid G, where a G-cosheaf is a localic cosheaf with an action by G (unitary and associative). Further aspects of categories of cosheaves will be discussed. In particular, a new construction of the symmetric topos (done in collaboration with Aurelio Carboni) will be discussed, whereby the symmetric topos of a topos X is given as the topos of sheaves on the lex completion of a (suitable) site of definition for X. Unpublished work of A.M.Pitts on the lex completion of a category with products is employed for this purpose.
Constructing parametric models of polymorphism Polymorphism enforces a type discipline on the normalizing terms of the lambda-calculus and its many extensions intend to improve the intuition about the behaviour of terms. Parametric polymorphism tries to extend an algebraic property at the first level of types to the higher types. But there seems to be still a striking difference between the syntax of polymorphism and its categorical models: the categorical models have produced only partial results in the direction of parametricity. The functorial contra/covariant behaviour of the type constructors has precluded a neat development of models. In particular, it is not known if there is a categorical parametric model. We review Ma and Reynolds's proposal for a semantic expression of parametricity, and recall the basic notions involved in this. In particular, their construction of the PL-category of relations over a given PL-category which is "suitable for parametricity". Then we present a new construction of a parametric completion for a PL-category: the basic idea is to use reflexive graphs of categories as introduced by O'Hearn and Tennent. The main theorem states that the parametric completion of a PL-category which is suitable for polymorphism satisfies parametricity (the proof uses Pitts's representation theorem). We discuss the result presenting some instances. Also, the construction is connected to relators and structors and we shall suggest possible modifications to include these. This is joint work with Edmund Robinson.
Categorie di Maltsev e teoria dei commutatori A category is called a Maltsev category if every reflexive relation is an equivalence; in the case of regular categories (in the sense of Barr) this property corresponds exactly to commutativity for the composition of equivalence relations. In my talk, I will first remind basic examples and properties of Maltsev categories and then I will study and characterize internal groupoids in this context. Mainly, I intend to show that it is possible to have a general theory of commutators, strongly related with the construction of the free groupoid on a reflexive graph.
Zermelo-Fraenkel algebras and bisimulation In this lecture we will use a general notion of bisimulation to construct categorical models of ZF set theory from an axiomatic theory of "small" maps (joint work with A. Joyal).
Duality and Synthetic Domain Theory This is an introductory presentation of the basic aspects of the Synthetic Theory of Scott Domains. We shall recall some general results about dualities based on an object Sigma. We then present some crucial examples where a "Sierpinsky" object Sigma enjoy very particular properties. These will allow to deduce fundamental results about a category of "Scott domains" such as the limit-colimit coincidence, and (a form of) algebraic compactness.
Evaluation Logic and Synthetic Domain Theory Evaluation Logic is an extension of predicate calculus with computational types and evaluation modalities. We shall recall previous attempts to interpret Evaluation Logic in categories of cpos, and discuss their limitations. Then we will show that, in the setting of Synthetic Domain Theory, it is possible to obtain an interpretation of Evaluation Logic starting from an interpretation for a programming language.
Co-inductive reasoning about functional programs The use of positive inductive definitions pervades the mathematical and logical foundations of computer science. The dual concept of co-inductive (or negative inductive) definition is also important, if somewhat less common. It often arises when constructing and reasoning about (potentially) infinite objects. Co-inductively defined equivalence relations (so-called `bisimulations') are commonly associated with the study of non-deterministic and concurrent computation. However, in this talk I hope to show that they can be a useful tool for reasoning about equality of more traditional, sequential functional programs.
Toposes as cocomplete categories In a recent joint work in collaboration with M. Bunge, we described the symmetric topos construction on a suitable 2-category A of cocomplete categories, in a purely `algebraic' way. As a gift, we were able to give a simple characterization of topos as cocomplete categories, which is totally internal to cocomplete categories, but uses the symmetric monad on A. The same of course applies to sup-lattices and frames too.
Homotopical algebra and triangulated categories This work studies the connections between an abstract setting for homotopical algebra, based on homotopy kernels and cokernels, and the well-known Puppe-Verdier notion of triangulated category. We show that a "right-homotopical" category A (having well-behaved homotopy cokernels, i.e. mapping cones) has a sort of weak triangulated structure with regard to the suspension endofunctor S, called S-homotopical category. If A is "homotopical" and "h-stable" (in a sense related to the suspension-loop adjunction), also this structure is h-stable, i.e. satisfies "up to homotopy" the axioms of Verdier for a triangulated category, excepting the octahedral one, which depends on some further elementary conditions on the cone endofunctor of A. Every S-homotopical category can be stabilised, by two universal procedures.
Objective Number Theory The possibility of encoding information about combinatorial objects into the geometry of complex numbers is often described as one of the mysteries of analysis. A demystifying tool was provided by S. H. Schanuel's Como paper (in SLNM 1488) "Negative sets have Euler characteristic and dimension" in the form of the functorial construction called the Burnside rig of a distributive category. Schanuel has recently showed that in a finite separable extension of the category of finite sets, the polynomial equations satisfied by the objects have in the complex numbers only integral roots, but that there are many combinatotial categories to which the result applies, for example directed graphs. But there are also "infinite" examples where abstract equations can be seen as a reflection of objective isomorphisms: for example the Euler product formula for the zeta function has behind it an isomorphism involving cartesian products of free monoids. My calculation showing that the "space" of binary trees has as Euler characteristic the complex number which is the primitive sixth root of unity, has recently been completed by A. Blass: seven-tuples of trees can be precisely coded as single trees by a very simple bijection, but if "7" is replaced by 5 or any number not congruent to 1 mod 6, such bijections can only be found in a category qualitatively more complicated.
Categorical Completeness Results for the Simply-Typed Lambda Calculus Let C be a cartesian closed category (where ccc = finite products + exponentials, not necessarily finite limits). The talk concerns conditions on C under which beta-eta conversion is complete for deducing all the equalities between terms of the simply-typed lambda calculus (with finite products and an arbitrary set of base types) which are validated by interpretations of the calculus in C. There are two natural forms of completeness: We say that C is COMPLETE (relative to beta-eta conversion) if, for all identically typed closed terms M, N, it holds that M and N are beta-eta equivalent iff, for all interpretations [.] of the lambda-calculus in C, [M] = [N]. (Categorically, C is complete if the class of ccc-functors from the free ccc, generated by the set of base types, to C is collectively faithful.) We say that C has a COMPLETE INTERPRETATION if there exists an interpretation [.] of the lambda-calculus in C such that, for all identically typed closed terms M, N, it holds that M and N are beta-eta equivalent iff [M] = [N]. (Categorically, C has a complete interpretation if there exists a faithful functor from the free ccc to C.) Examples. An interesting example of a CCC that has a complete interpretation is the category of sets (this is essentially Friedman's completeness theorem). Clearly any C that has a complete interpretation is also complete. The converse does not hold. For example, the category of finite sets is complete but has no complete interpretation. Further, not every ccc is complete. Trivially, any preorder that is cartesian closed (when viewed as a category) is not complete. In the talk I shall prove the following theorems, which give necessary and sufficient conditions for the two forms of completeness to hold. Theorem 1. C is complete if and only if it is not a preorder. Theorem 2. C has a complete interpretation if and only if it contains an endomorphism all of whose iterates are distinct.
Separable Objects and Coverings in Algebra and Geometry The general theory of separable objects in `good' categories will be discussed. This theory includes the theories of commutative separable algebras, of decidable objects in toposes and of covering spaces. The connection with general Galois theory in categories, and in particular with Grothendieck's Galois theory, will be considered.
Distributive adjoint strings For a string of adjoint functors V -| W -| X -| Y : B --> C, with Y fully faithful, it is often but not always the case that VY underlies an idempotent monad on B. Y has a profunctor right adjoint Z; it is equivalent to ask whether ZW is an idempotent (pro)comonad and sense for any `adjoint unity and identity of opposites'. We call such adjoint strings distributive, and give a wide variety of examples and a characterization. From a distributive string of length 3, such as W -| X -| Y, we can construct both longer and shorter distributive adjoint strings using profunctor calculus. This is joint work with R. J. Wood.