###Benedikt Ahrens (Birmingham) - invited tutorial {#ahrens}
“What is a space? - A univalent account”
###Mathieu Anel (Carnegie Mellon) - invited tutorial {#anel}
“What is a space? - An infinity-topos account”
###Ingo Blechschmidt (Verona) - invited speaker {#blechschmidt}
“A general Nullstellensatz for generalized spaces”
The Nullstellensatz of commutative algebra states that some algebraic truths are witnessed by explicit algebraic certificates, syntactical a priori reasons for why a given truth is to be expected.
We discuss a logical analogue of the Nullstellensatz, valid for the generic model of any geometric theory. This analogue replaces algebraic certificates by logical certificates – geometric proofs. It is a source of nongeometric sequents enjoyed by generic models, and it turns out that it is the universal such source.
###Auke Booij (Birmingham) {#booij}
“Extensional constructive analysis via locators”
Real numbers do not admit an extensional procedure for observing discrete information, such as the first digit of its decimal expansion, because every extensional, computable map from the reals to the integers is constant, as is well known. We overcome this by considering real numbers equipped with additional structure, which we call a locator. With this structure, it is possible, for instance, to construct a signed-digit representation or a Cauchy sequence, and conversely these intensional representations give rise to a locator. Although the constructions are reminiscent of computable analysis, instead of working with a notion of computability, we simply work constructively to extract observable information, and instead of working with representations, we consider a certain locatedness structure on real numbers.
###Olivia Caramello (Como) - invited speaker {#caramello}
“Denseness conditions and equivalences of toposes”
We shall present a theorem providing necessary and sufficient conditions for a morphism of sites to induce an equivalence of toposes, and discuss a number of applications.
###Francesco Ciraulo (Padova) {#ciraulo}
“Weak closure, Strong density: an overtview”
The notion of a closed subset in formal topology corresponds to that of an overt weakly closed sublocale. Accordingly, a binary positivity predicate (in the sense of Sambin) on a formal topology corresponds to a suplattice of points of its lower powerlocale (C.-Vickers). Such a point of view illuminates the connection between locales and “positive topologies” (formal topologies with binary positivity; see Maschio’s talk) and allows us to calculate (co)limits of positive topologies (C.-Kawai-Maschio), at least in an impredicative framework.
A weak notion of closure corresponds to a strong notion of density, of course. It is a fact that every locale has a smallest strongly dense sublocale (Johnstone); and if the locale is overt, than such a sublocale happens to be an “overlap algebra” (as defined by Sambin). So, classically, an overlap algebra is precisely a complete Boolean algebra; and many results on Boolean locales have a (constructive) version in terms of overlap algebras. Time permitting, we will also show some recent results about the category(-ies) of overlap algebras.
###Maria Manuel Clementino (Coimbra) - invited speaker {#clementino}
“Revisiting generalised enriched categories”
For a commutative and unital quantale V and a Set-monad T laxly extended to V-Rel, the notion of (T,V)-category is both a generalisation of a (V-)enriched category and a lax version of an Eilenberg-Moore T-algebra. As main examples of (T,V)-categories we mention topological spaces, Lawvere metric spaces, ultrametric spaces, Lowen approach spaces, and probabilistic metric spaces. Together with (T,V)-functors, they form a topological category over Set, which, under mild conditions, is (infinitely) extensive. Moreover, it is weakly cartesian closed, and therefore its exact completion is cartesian closed.
In this talk we will present this general setting, and then concentrate on the proof of its weak cartesian closedness. This will be an excuse to make a detour through interesting notions and results, like representability, injectivity, Cauchy-completeness, and a generalised Yoneda embedding.
###Thierry Coquand (Chalmers) {#coquand}
“Constructive mathematics and higher topos theory”
I will present a modification of the model of binary choice sequences (as described in the work of Chuangjie Xu and Martin Escardo) in a way which stresses its analogy with the Zariski topos. I will then explain how to modify this model in order to get a model of binary choice sequences together with dependent type theory and univalence (higher topos?), and conclude by some remarks on one potential use of higher topos theory for constructive mathematics.
“Regular entailment relations”
This is joint work with Henri Lombardi and Stefan Neuwirtz and was motivated by an attempt to understand some results of Lorenzen. I will present a notion of entailment relations which corresponds to lattice ordered groups. In particular, a cut elimination theorem in this setting may be seen as the justification of the classical result that any lattice ordered groups can be embedded in a product of linearly ordered groups.
###Martin Escardo (Birmingham) {#escardo}
###Eric Finster (Birmingham) {#finster}
“Spectra as Infinitesimal Homotopy Types”
Cohomological invariants play a fundamental role in modern algebraic topology as they strike a reasonable balance between power and computability. The Brown Representability theorem asserts that the functors assigning to a space its (generalized) cohomology groups are always representable, and the respresenting objects are called spectra. Inspired by Goodwillie’s calculus of homotopy functors, it is possible to think of spectra as “infinitesimal” homotopy types. I will develop this analogy and explain how it can be implemented in homotopy type theory.
###Sina Hazratpour (Birmingham) {#hazratpour}
“Fibrations of toposes”
(Joint work with Steve Vickers)
Fuller pdf abstract with references
The notions of (op)fibration of toposes have close connections to topological properties. For instance, every local homeomorphism is an opfibration. This connection is in line with the conception of toposes as generalized spaces. To study fibrations of toposes, Johnstone defined fibrations internal to 2-categories ([2]). If toposes are taken to be bounded over some fixed base S, the analysis of fibrations and opfibrations in the 2-category BTop/S of bounded toposes over base S is much easier than the general case where there is no canonical choice of base topos and one has to work in the 2-category BTop. Indeed, Johnstone proved several important (op)fibrational results in BTop.
I will introduce the 2-category Con of contexts developed by Vickers ([3],[4]). It provides a language to reason about geometric construction within the predicative fragment of internal language of toposes, that is within the language of Arithmetic Universes. Borrowing from work of Street ([1]), we introduce a syntactic notion of (op)fibration in Con which is based on Chevalley’s internal characterization of fibrations obtained as a theorem in there.
Note that Johnstone’s definition of internal (op)fibrations is more general than Chevalley’s definition: neither strictness of 2-categories nor the existence of the structure of strict pullbacks and comma objects are assumed. I shall explain our result that gives a recipe for obtaining (op)fibrations of toposes from the finitary syntactic (op)fibrations of contexts ([5]). The scaffolding of the proof of this result is based on a certain comprehension bicategory involving fibred bicategory of generalized spaces over elementary toposes. I will discuss the application of this result to construction of colimits of topos and bag toposes from generalized point-free point of view.
###Hajime Ishihara (JAIST) {#ishihara}
“Equivalents of the finitary non-deterministic inductive definitions”
We present statements equivalent to some fragments of the principle of non-deterministic inductive definitions (NID) by van den Berg (2013), working in a weak subsystem of constructive set theory CZF. We show that several statements in constructive topology which were initially proved using NID are equivalent to the elementary and finitary NID. We also show that the finitary NID is equivalent to its binary fragment and that the elementary NID is equivalent to a variant of NID based on the notion of biclosed subset. Our result suggests that proving these statements in constructive topology requires genuine extensions of CZF with the elementary or finitary NID.
This is a joint work with Ayana Hirata, Tatsuji Kawai and Takako Nemoto.
###Peter Johnstone (Cambridge) - invited speaker {#johnstone}
“Betweenness reals: How to do Dedekind cuts when you don’t know which way is up”
Recently Vaughan Pratt claimed on the categories list that any of the standard constructions of the reals from the rationals could be carried out using only the affine-space structure of the rationals. As I pointed out at the time, that is not quite true, because the Dedekind-cuts construction makes essential use of the order-relation on Q, which is not definable from the affine structure since Q has order-reversing affine automorphisms. However, Q does have a ternary ‘betweenness’ relation definable from its affine structure. In this talk I shall investigate how the Dedekind-cuts construction can be made to work for spaces equipped with a betweenness structure: the results are mostly predictable, but there are one or two unexpected twists.
###Milly Maietti (Padova) {#maietti}
“On the constructivity of the notion of formal space”
One of the peculiar properties of the Minimalist Foundation, for short MF, ideated in [MS05] and completed in [M09], is that the well known representations of real numbers do not form a set. Therefore, as argued in [MS13], a point-free notion of space like that of formal topology, or better that of Sambin’s Positive topology, seems compulsory to represent the topology of the Continuum.
A key benefit of developing topology in MF is that it enjoys a strong constructivity requirement proposed in [MS05].
This can be shown for MF, possibly extended with inductive and coinductive definitions necessary to represent relevant genuine examples of positive topologies, thanks to [IMMS18] and work by M. Rathjen.
As a byproduct, jointly with S. Maschio, we employ some categorical constructions in [MR13] to build a predicative version of Hyland’s Effective Topos (which embeds into it) where to extract programs from proofs done in the mentioned extension of MF.
This construction can be put in relation with the notion of arithmetic universe in Vickers’s work.
[MS05] Maietti M.E., Sambin G.: Toward a minimalist foundation for constructive mathematics. In: L. Crosilla and P. Schuster (ed.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, no. 48 in Oxford Logic Guides, pp. 91-114. Oxford University Press (2005)
[M09] Maietti M.E.: A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic 160(3), 319-354 (2009)
[IMMS18] Ishihara H., Maietti M.E., Maschio S. , Streicher T. : Consistency of the intensional level of the Minimalist Foundation with Church’s thesis and Axiom of Choice. Archive for Mathematical Logic, 57(7-8):873-888, 2018
[MR13] Maietti M.E. , Rosolini G. : Elementary quotient completion. Theory and Applications of Categories, 27(17):445-463, 2013
[MS13] Maietti M.E., Sambin G.: Why topology in the Minimalist Foundation must be pointfree. Logic and Logical Philosophy 22,167-199,2013
###Graham Manuell (Edinburgh) {#manuell}
“The spectrum of a localic semiring”
Some important notions of spectrum include the Stone spectrum of a distributive lattice, the Zariski spectrum of a ring, the Gelfand spectrum of a C*-algebra and the Hofmann-Lawson spectrum of a distributive continuous lattice. Each of these assigns a space of closed prime ideals to a certain kind of topological semiring – or in the constructive setting, they assign locales to certain localic semirings. We present a general theory of spectra for localic semirings. Such a spectrum need not always exist, but we will discuss conditions under which it does.
###Samuele Maschio (Padova) {#maschio}
“Factorizing the Top-Loc adjunction through positive topologies”
(Joint work with Francesco Ciraulo and Tatsuji Kawai)
We characterize the category of Sambin’s positive topologies as a fibration over the category of locales Loc. The fibration is obtained by applying the Grothendieck construction to a doctrine over Loc. We then construct an adjunction between the category of positive topologies and that of topological spaces Top, and show that the well-known adjunction between Top and Loc factors through the newly constructed adjunction.
###Paige North (Ohio) {#north}
“Constructing models of homotopy type theory with abstract real numbers”
This talk presents progress towards understanding categorial interpretations of homotopy type theory and directed homotopy type theory. Such interpretations require ‘type theoretic’ or ‘directed type theoretic’ weak factorization systems in the target category. I will talk about generalizations of the construction of such a weak factorization system in topological spaces using the Moore path space.
###Erik Palmgren (Stockholm) {#palmgren}
“Localic completions in constructive analysis”
Formal topology may be regarded as locale theory developed within a neutral constructivist framework, such as that of Bishop’s constructive mathematics [1], avoiding impredicativity and the principle of excluded middle. A systematic investigation was started by Martin-Lof and Sambin [5] using type theory as foundation. A link between formal topology and Bishop’s theory of compact metric spaces was provided by Vickers’ seminal notion of localic completion [3, 4]. With Vickers’ method it can be shown [2] that the category of open subspaces of locally compact metric spaces embed fully faithfully into the category of locales (or formal topologies). This gives the possibility to apply methods of locale theory to constructive analysis, and conversely prove certain results about locales using point-based methods.
[1] E. Bishop and D.S. Bridges, Constructive Analysis. Springer 1985.
[2] E. Palmgren. Open sublocales of localic completions. Journal of Logic and Analysis. 2:1(2010), 1 - 22.
[3] S. Vickers. Localic completion of generalized metric spaces I, Theory and Applications of Categories 14(2005), 328 - 356.
[4] S. Vickers. Localic completion of generalized metric spaces II, Journal of Logic and Analysis 1:11(2009), 1 - 49.
[5] G. Sambin. Intuitionistic formal spaces - a first communication, in: D. Skordev (ed.), Mathematical logic and its Applications, Plenum Press 1987, pp. 187 - 204.
###Pedro Resende (IST Lisbon) {#resende}
“The observational logic of quantum mechanics”
I shall revisit Steve’s thirty year old idea that quantales provide an algebraic logic of run-time observations on systems whose states may change when they are observed. This is a natural generalization of the view of locales as mathematical descriptions of the finitely observable properties of computational systems, and it has been applied in computer science to the study of concurrent processes.
However, the term “quantale” was coined a few years earlier by Mulvey in a different context, where quantales were meant to play the role of spectrum for noncommutative C*-algebras in a way that extends the Gelfand-Naimark representation theorem.
Either way, the idea that quantales may have something interesting to tell us about quantum theory comes to mind, and the purpose of this talk is to explore this via stably Gelfand quantales and their interplay with étale groupoids and inverse semigroups. A notion of classical observer appears naturally, along with quantum concepts such as superposition, entanglement and complementarity, and the model obtained can be regarded as a purely topological facet of quantum mechanics that ought to relate to the standard probabilistic theory in roughly the same way that measure theory sits on topology.
###Claudio Sacerdoti Coen (Bologna) {#coen}
###Giovanni Sambin (Padova) - invited speaker {#sambin}
“Half way to Grothendieck’s aim”
Formal topology was born to show in practice that one can develop mathematics over a truly predicative foundation.
Besides achieving this, the present formulation of formal topology offers a rigorous proof to the expectation, that is present since the time of Grothendieck, of an embedding of pointwise topology into pointfree topology. Thus it provides good motivations also for mathematicians.
Using a “weak” foundation to develop topology, one is compelled to preserve more information than usual, and thus replace topological spaces with “concrete spaces”, and locales (or formal topologies) with “positive topologies”.
Contrary to a common expectation, it is precisely this “useless” information that offers a solution to Grothendieck’s aim. In fact, the link between pointfree and standard topology (with points), usually expressed by the categorical adjunction between topological spaces and locales, is refined into a categorical embedding of concrete spaces into positive topologies. This embedding does not look possible without exploiting the presence of the new notion of positivity relation.
Half way because locales or formal topologies can be seen as Grothendieck topologies over an ordered category, and thus the above embedding leaves the problem open of finding a suitable notion of positivity (alias closed subsets) in the framework of arbitrary Grothendieck topologies.
###Christopher Townsend {#townsend}
“History of the double power locale”
I will trace, very broadly, the various power constructions and results that were precursors to the double power locale construction. I will then remind the audience of some of the key properties of the double power locale - which make it such an interesting construction - notably its role in (i) formalising the duality between compact and discrete; and, (ii) representing geometric morphisms as structure preserving maps.
###Steve Vickers (Birmingham) {#vickers}
“Toposes via arithmetic universes”
I take it that the distinctive feature of point-free topology, applying equally to locales and to formal topology, is that the points of a space are given not as elements of a set (point-set topology), but as models of a geometric theory. This frees up the points and allows them to live in categories other than one’s favourite category of sets.
It also opens up the generalization to predicate theories, giving the generalized spaces for which Grothendieck invented toposes.
Already there are two different semantic notions for what a ‘generalized space’ might be: one of the original Grothendieck toposes; or a bounded geometric morphism to an elementary topos chosen as one’s ‘favourite category of sets’.
I shall describe a third semantic notion using arithmetic universes, and how they can be used to give constructive base-independent proofs about toposes. I shall also say something about the challenges if they are to be more than just a toy model of generalized spaces, and to provide any of the machinery for which Grothendieck invented toposes.