Organisers: Loïc Pujet, Peter LeFanu Lumsdaine, Anders Mörtberg, Per Martin-Löf (emeritus)
The regular seminar time is Wednesdays 10.00–12.00, and the usual location is floor 3, Room U (Kovalevsky), Albano house 1 (Greta Arwidssons Väg 30), Stockholm.
11:30–17:30
Joint Stockholm–Göteborg type theory seminar, Albano Hus 1, rooms 12 (first talk) and 23 (afternoon talks).
Schedule:
Anders Mörtberg, Stockholm
The category of iterative sets in homotopy type theory and univalent foundations
Abstract: When working in HoTT/UF the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of Set hold for hSet ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, the univalence axiom implies that Ob(hSet) is not itself an h-set, but an h-groupoid. This is expected in univalent foundations, but it is sometimes useful to also have a stricter universe of sets, for example when constructing internal models of type theory. To this end we equip the type of iterative sets V⁰, due to Gylterud (2018) as a refinement of the pioneering work of Aczel (1978) on universes of sets in type theory, with the structure of a Tarski universe and show that it satisfies many of the good properties of h-sets. In particular, we organize V⁰ into a (non-univalent strict) category and prove that it is locally cartesian closed. This enables us to organize it into a category with families with the structure necessary to model extensional type theory internally in HoTT/UF. We do this in a rather minimal univalent type theory with W-types, in particular we do not rely on any HITs, or other complex extensions of type theory. Furthermore, the construction of V⁰ and the model is fully constructive and predicative, while still being very convenient to work with as the decoding from V⁰ into h-sets commutes definitionally for all type constructors.
This is joint work with Daniel Gratzer, Håkon Gylterud, and Elisabeth Stenholm and a preprint is available at arXiv:2402.04893
Freek Gerligs, Göteborg
Synthetic Stone duality
Abstract: We present an axiomatization for higher light condensed sets in HoTT-UF, similar to the axiomatization of the higher Zariski topos in synthetic algebraic geometry. In the resulting theory, we are able to prove the limited principle of omniscience and Markov's principle. However, the weak limited principle of omniscience is provably false. Furthermore, we have a definition of compact Hausdorff spaces and can show that all maps between compact Hausdorff spaces are continuous.
Work by: Felix Cherubini, Thierry Coquand, Freek Geerligs and Hugo Moeneclaey.
Gabriel Saadia, Stockholm
B-systems as a strict axiomatization of natural models
Abstract: In 2014 Voevodsky introduced B-systems as an axiomatization of contextual categories that is as close to the syntax of Martin-Löf type theory as possible. His objective was to find a uniform way to produce and to understand initiality theorems.
Jonas Höfer, Göteborg
Poset Type Theory
Abstract: This is jww Thierry Coquand, Jonas Höfer.
Our work is motivated by a recent construction of a model of univalent type theory by Sattler (a description of which can be found in [C, S]). This construction is done in two steps. One instance of the first step, is a cubical model based on presheaves over finite, non-empty posets. In a second step, a new model of type theory is obtained by localizing along a lex modality. This second model validates Whitehead’s principle, and dependent choice. Furthermore, it is expected to give a good constructive notion of homotopy types of spaces.
We design a cubical type theory based on the first model, which can be interpreted in the second model as well. As a cubical type theory, it supports homogeneous composition and coercion between arbitrary endpoints, connections, and diagonal cofibrations. This makes it an extension of both Cartesian cubical type theory [ABCFHL], and the Dedekind version of CCHM [CCHM]. We have written a corresponding type checker and evaluator for this type theory (https://github.com/JonasHoefer/poset-type-theory). Furthermore, we conjecture it to have good meta theoretical properties, such as normalization and decidability of type checking. Lastly, this work is a first step towards a type theory for the localized model that validates the additional reasoning principles.
Errol Yuksel, Stockholm
Toposes as stacks
Abstract: In algebraic geometry, after having defined schemes one usually goes on to define higher-dimensional notions such as algebraic spaces, algebraic stacks, and Deligne-Mumford stacks. I will recall the general form of these definitions and adapt it to the case of locales, essentially replacing schemes by locales. The resulting objects, which might be called localic stacks, are thus a generalisation of locales one dimension up. Toposes can also be seen as such a generalisation, and I will explain the relation between the two (for instance every topos is a localic stack).
Oskar Eriksson, Göteborg
Graded modal type theory for linear and affine types with recursive functions
Abstract: Graded modal type theory can be used to encode information about variable uses into types making it possible to express, for instance, linear or affine typing. Myself, Andreas Abel and Nils Anders Danielsson have been developing an Agda formalisation of such a type theory with recursion over natural numbers, proving consistency, normalisation, and decidability of typing. In this talk, I will describe my work on extending this formalisation by an abstract machine with a resource-aware heap. This heap semantics shows that graded modal type theory correctly captures the notions of linear and affine types, in particular, preventing linear variables from being accessed more than once.
10.00–12.00
Peter Lumsdaine, Stockholm University
Classifying toposes for fun and profit
Abstract: This will be an expository talk, illustrating how topos-theoretic techniques can be
applied to turn non-constructive model-theoretic proofs into concrete proof-theoretic arguments.
As the central example, I will take Parikh’s proof (using non-standard models) that if φ(x,y) is
a bounded (i.e. Δ₀) formula of arithmetic, and “for all x, there exists y such that φ(x,y)” is
provable from just induction for Δ₀ formulas, then there is some fixed k such that this
existence is provably bounded by xᵏ.
10.00–12.00
Loïc Pujet, Stockholm University
Church's Thesis in Type Theory
Abstract: The internal Church Thesis states that all integer functions are computable by Turing
Machines. Together with Markov's principle, it is one of the defining principles of the Russian
school of constructive mathematics.
This might not sound very surprising to a type theorist: after all, in Martin-Löf's Type Theory,
functions *already* are programs. Thus, one may internalise Church's Thesis by extending the
language with a "quote" operator that reifies the code of functions. However, although this
strategy is quite natural from a programming perspective, the existence of quote has surprising
consequences on the logic, and it is not clear the the resulting system is consistent.
In this talk, I will discuss some of the consequences of Church Thesis in Martin-Löf's type
theory, and I will go over Pédrot's recent proof of consistency.
10.00–12.00
Axel Ljungström, Stockholm University
Steenrod squares, the HoTT way
Abstract: The Steenrod squares (Sq^n) form a set of cohomology operations which can,
among other things, be useful for distinguishing different spaces whose cohomology
rings happen to be the same. In this talk, I will show you how to construct these in
homotopy type theory (HoTT) and how one very simple (but, it turns out, surprisingly
hard to prove) Fubini-like theorem for unordered joins implies both the so-called
Cartan formula and the Adem relations. I will also discuss how the proofs of the
suspension axiom and Sq^0(x) = x can be reduced to a computational problem and
thereby give rise to a new Brunerie number. Finally, I might say a word or two about
why the higher Steenrod powers are so hard to define in HoTT (coherence problems?
You bet!).
This is joint work with David Wärn.
11.00–12.30
Max Zeuner, Stockholm University
Some more synthetic algebraic geometry
Abstract: This talk is a continuation of last week's introduction to synthetic algebraic geometry. The plan is to discuss more non-classical consequences of the axioms and see example of non-affine internal schemes such as the projective spaces P^n. Furthermore we want to look at how étale maps and smooth schemes can be described internally through the use of modalities (in the homotopy-type-theoretic sense).
11.00–12.30
Max Zeuner, Stockholm University
What is synthetic algebraic geometry?
Abstract: Synthetic algebraic geometry (SAG) is generally speaking the study of algebro-geometric objects in the internal logic of the so-called big Zariski topos. Complicated sheaf-theoretic constructions often become fundamental algebraic constructions from the internal point of view and this can be used to simplify and shorten proofs. A central role is taken by the affine line A^1, which internally looks like a ring with very surprising, anti-classical properties. In fact, it is possible to develop SAG axiomatically in a constructive meta-theory by stipulating a ring sharing some key properties with the internal affine line. An ongoing project at Chalmers university develops this axiomatic approach to SAG, using homotopy type theory (HoTT) as the constructive meta-theory. The purpose of this talk is to give the necessary background on the big Zariski topos and a basic introduction to axiomatic SAG. If time permits, I would also like to discuss the benefits of working in HoTT (namely being able to define cohomology) and sketch a purported model construction using "cubical Zariski sheaves".
11.00–12.30
Iosif Petrakis, Università di Verona
From dependent type theory to dependent category theory
Abstract: We introduce categories with dependent arrows, in order to grasp type-dependency in categorical terms. As arrows are categorical generalisations of functions, dependent arrows are categorical generalisations of dependent functions in Martin-Löf Type Theory. We present results first in the theory of categories with dependent arrows and Sigma-objects, and second in the theory of (the introduced) dependent fibrations between them. In this way we generalise results in the theory of type-categories of Pitts, and the theory of fibrations between them, respectively. All introduced notions, examples, and shown results have their dual version.
11.00–12.30
Peter LeFanu Lumsdaine, Stockholm University
Fraenkel–Mostowski models are continuous G-sets, or something like that
Abstract:
Fraenkel–Mostowski permutation models are a straightforward but flexible technique for independence results in set theory, giving models of ZFA (set theory with atoms). Categorically, these can be viewed as arising from a topos of continuous G-sets, or alternatively as a slight modification of this (as noted by Fourman, Blass, and Scedrov).
Why are there two possible toposes corresponding to this model? What does the difference between them mean, either as toposes in their own right or in terms of their connection to set-theoretic Fraenkel–Mostowski models?
I’ll recall all of these constructions and compare them, largely following Blass–Scedrov, but partly also in the more recent light of Shulman’s stack semantics.
11.00–12.30
Loïc Pujet, Stockholm University
Pre-fascism and the thin blue cubes (part 2)
Abstract: This will be the continuation of my seminar from last week. Last time, I explained the construction of Pédrot's "prefascist sets", and to which extent they are a strict replacement for presheaves. Now I will go over their applications, in particular for the construction of internal models for type theory.
11.00–12.30
Loïc Pujet, Stockholm University
Pre-fascism and the thin blue cubes
Abstract:
Presheaves are a fundamental construction in category theory, and the basis of the cubical models of univalence. But interestingly enough, presheaves do not play so well with homotopy type theory: because of the higher dimensional structure of types, a correct definition of a Type-valued functor requires infinitely many coherence equations.
In his paper [Russian Constructivism in a Prefascist Theory], Pédrot introduces the "prefascist sets", a strictified presentation of presheaves: they satisfy the functoriality equations definitionally, and thus they automatically have all the higher coherence laws. Pédrot then uses prefascist sets to give a presheaf model of type theory internally to type theory.
In this talk, we will dissect Pédrot's construction, build higher dimensional variations, and use fibrant prefascist sets to give an internal model of univalence in observational type theory.
10.00–12.00
Philip Hackney, University of Louisiana at Lafayette
Induced model structures on cubical sets
Abstract: Quillen model categories are a particularly structured way to encode higher homotopical structure. It is advantageous to construct new model structures from existing ones, and there are a number of techniques to do so. For instance, if F: N → M is a functor with M a model category, it is sometimes possible to put a model structure on N where some parts of the structure lifted from the model structure on M. I'll explain simple criteria guaranteeing that such "induced" model structures exist in the special case when the functor F is both a right and a left adjoint. We'll apply these criteria to a category of cubical sets, giving model structures for ∞-groupoids and ∞-categories. This talk is based on joint work with Martina Rovelli.
10.00–12.00
Loïc Pujet, Stockholm University
Indexed inductive types in Observational Type Theory
Abstract:
Observational Type Theory (OTT) was designed by Altenkirch, McBride and Swierstra to extend MLTT with function extensionality and the uniqueness of identity proofs, while preserving most of its computational properties. It can be thought of as a type theory for setoids with a proof-irrelevant equality, just like Cubical Type Theory is a type theory for fibrant cubical sets.
The aim of this talk is to present joint work with Nicolas Tabareau on implementing OTT in the Coq proof assistant. In particular, I will explain how we handle the full scheme of indexed inductive types of Coq, without breaking compatibility with the existing Coq syntax.
10.00–12.00
Max Zeuner, Stockholm University
Geometric and functorial schemes from the constructive predicative viewpoint
Abstract: Schemes are usually defined using locally ringed spaces but for algebraic geometers it can be more convenient to work with the functor of points associated to a scheme. In fact, Grothendieck favored the approach of defining schemes directly as certain well-behaved functors from rings to sets. These "functorial schemes" are easily shown equivalent to the "geometric schemes" defined through locally ringed spaces. In this talk we look at how much of this picture can be recovered when working constructively and predicatively.
10.00–12.00
Evan Cavallo, Stockholm University
Unifying cubical type theories
Abstract: The push to find a computational interpretation for homotopy type theory led to the development first of multiple models of HoTT based on cubical sets, then corresponding cubical type theories which can serve as computational alternatives to HoTT. The various type theories and models appear similar, but are not self-evidently instances of some single family of theories or model construction. I will present joint work with Anders Mörtberg and Andrew Swan from 2020 which unifies the so-called "structural" cubical theories and models, giving a parameterized definition which can be applied with different choices of interval structure and cofibrations. I will also discuss the still-open problems in this area, such as the case of substructural cubical models.
10.00–12.00
Thomas Lamiaux, ENS Paris-Saclay
Introduction and Unification of Different Approaches to Initial Semantics
Abstract:
Initial semantics aim to categorically represent programming languages as initial models, in order to axiomatise their syntax and substitution structures. To do so automatically, it relies on initiality theorems, that assert under simple conditions, if a programming language have an initiality model.
Initial semantics has been historically separated in three different traditions: one based on Marcello Fiore's work, one based on modules over monads and one based on heterogeneous substitution systems and signatures with strength. Noticeably, the different framework are poorly related to each other, and there is no clear introduction to any traditions.
In this talk, I give an introduction to initial semantic, and present our work, with Benedikt Ahrens, to write a clear presentation clarifying and unifying those traditions.
10.00–12.00
Eric Finster, University of Birmingham
The Baez-Dolan +-Construction for Generalized Algebraic Theories
Abstract:
The Baez-Dolan +-construction is an operation on symmetric operads which produces, from a given operad O, a new operad O+ whose algebras are operads equipped with a map to O. Iteratively applying this construction to the identity operad, whose algebras are just sets, generates a family of polytopes (the "opetopes") which play a central role in Baez and Dolan's approach to higher algebra.
In this talk, I will discuss the application of Baez-Dolan construction to arbitrary generalized algebraic theories and outline some possible applications.
10.00–12.00
Morgan Rogers, Laboratoire d’Informatique Paris Nord
Endomorphisms of models: yet another categorification of model theory
Abstract: Model theory has inspired a wide spectrum of developments in category theory, often with a goal of recasting this very set-theoretic domain in a categorical framework. This vein still has plenty of ideas to mine, of which I shall present one originally suggested to me by the late Pieter Hofstra: the correspondence between closed subgroups of the (topological) automorphism group of a set and extensions of that set by relations. We recast this in terms of classifying toposes, and show how this enables us to restate the result with monoids in place of groups and almost arbitrary structures in place of sets.
10.00–12.00
Anders Mörtberg, Stockholm University
The Category of Iterative Sets in Univalent Foundations
Abstract: When working in HoTT/UF the category of h-sets is traditionally used as a univalent version of the category of sets. One consequence of this is that one gets a 1-type of objects instead of an h-set. This is often what one wants in univalent mathematics, but for some applications it is better to give up univalence in favor of an h-set of objects. There are many constructions of such set universes in HoTT/UF and a particularly elegant one is Gylterud's refinement of Aczel's 1978 universe of sets V which is based on W-types. In the talk I will report on ongoing work with Bonnevier, Gratzer and Gylterud to analyze Gylterud's universe from a category theoretic perspective, with the aim of formalizing models of type theory inside of HoTT/UF.
10.00–12.00
Ivan Di Liberti, Stockholm University
Lindström in fabula
Abstract: Lindström-type theorems are a paradigm of theorems that characterise fragments of logic among other logical system by identifying pivotal properties. The original theorem due to Lindström identifies first order logic as the minimal logic enjoying both compactness and Löwenheim-Skolem theorem. After an historical overview of Lindström-type theorems, we will see its incarnation in the 2-category of topoi, where Lindström theorem emerges tautologically as the very definition of coherent logic. Time permitting, we shall comment on Pitts’ approach to Craig interpolation theorem and its relevance in this story.
10.00–12.00
Axel Ljungström, Stockholm University
Dealing With Smash Products in HoTT
Abstract:
Verifying that the smash product forms a symmetric monoidal product in HoTT turns out to be rather complicated. There is no deeper reason for this: it should, in theory, follow by induction. However, the number of coherences which need to be verified grows too quickly for anyone in their right mind to actually complete the proof. Some solutions have been suggested: van Doorn (2018) attacked the problem by an argument using closed monoidal categories while Brunerie (2018) attempted to produce a computer generated proof using Agda meta-programming. Unfortunately, van Doorn left a gap where the path algebra got too involved and Brunerie's generated proof failed to type-check due to it eating up far too much memory.
In this talk, we choose a different line of attack by introducing a heuristic for proving equalities of pointed maps defined over iterated smash products. With this heuristic, we significantly bound the number of coherences appearing in such proofs. In particular, this heuristic lets us prove that smash products are symmetric monoidal in a rather straightforward manner.
10.00–12.00
Max Zeuner, Stockholm University
Locally ringed lattices - a constructive approach to quasi-compact, quasi-separated schemes
Abstract: In this talk we introduce the category of locally ringed lattices. We will show that this is equivalent to a subcategory of locally ringed spaces, which contains quasi-compact, quasi-separated schemes as a full subcategory. We will then show how this category of locally ringed lattices can be used as the basis of a point-free and constructive development of algebraic geometry. In particular, we will give a constructive proof that the functor "Spec" taking a commutative ring R to the locally ringed lattice corresponding to the affine scheme Spec(R) is left adjoint to the global sections functor. We will also give a definition of quasi-compact, quasi-separated schemes in this setting and discuss examples of non-affine schemes if time permits.
10.00–12.00
Taichi Uemura, Stockholm University
Cubical assemblies models of type theory
Abstract:
The assemblies model of type theory has an impredicative universe and satisfies principles of constructive recursive mathematics. The cubical assemblies, cubical objects in the assemblies model, form a model of type theory which is naturally expected to have an impredicative and univalent universe and satisfy principles of constructive recursive mathematics.
In this talk, we will study the cubical assemblies model and related models. The cubical assemblies model DOES have an impredicative and univalent universe. This universe does NOT admit propositional resizing. The cubical assemblies model does NOT satisfy Church's thesis, one of the most important principles of constructive recursive mathematics. A localization of the cubical assemblies model DOES satisfy Church's thesis. Another localization of the cubical assemblies model DOES satisfy a version of extended Church's thesis.
Most part of this talk is about earlier work of Andrew Swan and myself. The result on extended Church's thesis has recently been shown by Swan (arXiv:2209.15035).
10.00–12.00
Peter LeFanu Lumsdaine, Stockholm University
The cumulative hierarchy in type theory
Abstract:
In ZF(C) and similar material set-theoretic foundations, the cumulative hierarchy of iterative sets provides the arena in which all mathematics takes place. In other foundations, is place is less central; but it still exists, as a rich and useful structure.
In this talk, I will survey several treatments of the cumulative hierarchy and variants in type theory and related settings, including some or all of:
- Aczel’s type of iterative sets
- Palmgren’s applications of this in “From type theory to setoids and back”
- Gylterud’s adaptation of it to multisets
- Moerdijk and Joyal’s “Algebraic set theory” characterisation of the cumulative hierarchy
- the HoTT book’s presentation of the cumulative hierarchy as a higher inductive type.
10.00–12.00
Peter LeFanu Lumsdaine, Stockholm University
Mahlo universes
Abstract: This will be a continuation from my seminar last-week-but-one, on large cardinals as seen from type theory — in particular, surveying results of Setzer, Dybjer, Palmgren, and others, and comparing different characterisations of Mahlo cardinals/universes.
10.00–12.00
Brandon Doherty, Stockholm University
A cofibration category of directed graphs
Abstract: Cofibration categories are categories equipped with designated classes of morphisms, called cofibrations and weak equivalences, satisfying certain properties which allow for the convenient construction of a homotopy category. Similar in concept to model categories, though weaker, cofibration categories (suitably defined) present homotopy theories having all small homotopy colimits. In this talk, based on ongoing joint work with Carranza, Kapulkin, Opie, Sarazola, and Wong, I will describe a new cofibration category structure on the category of directed graphs, whose weak equivalences are maps inducing isomorphisms on the path homology groups defined by Grigor’yan, Lin, Muranov, and Yau.
10.00–12.00
Peter LeFanu Lumsdaine, Stockholm University
Large cardinals in type theory
Abstract:
This will be an expository seminar, surveying results of Dybjer, Setzer, and Palmgren (and possibly others).
Large cardinals are a mainstay of classical set theory, and are often thought of as its of little interest beyond it. However, at least some large cardinal principles turn out — unsurprisingly, in hindsight — to correspond to natural largeness conditions on universes in type theory, phrased in terms of closure under various type-forming constructions. I will introduce and survey the best-understood such connections and their implications, in particular the correspondence (established by Dybjer and Setzer) between Mahlo cardinals and universes closed under formation of inductive-recursive types.
10.00–12.00
Henrik Forssell, Oslo Metropolitan University
The coherent definability theorem by locales of models
Abstract: In his PhD Thesis, Johan Lindberg gave an explicit description of the Joyal-Tierney representation theorem in terms of locales of models of geometric theories. We revisit this description and show an example application of it by giving a constructive formulation and proof of the Definability Theorem for coherent logic (Elephant, D3.5.1).
10.00–12.00
Ivan Di Liberti, Stockholm University
The geometry of coherent topoi and ultrastructures
Abstract: It is know that for T a first order theory we can construct ultraproducts of models along ultrafilters. From a topos theoretic point of view, this property should correspond to a geometric property of coherent topoi. We discover such geometric property and we see how that impacts the behavior of coherent topoi. We show that coherent topoi are right Kan injective with respect to flat embeddings of topoi. We recover the ultrastructure on their category of points as a consequence of this result. We speculate on possible notions of ultracategory in various arenas of formal model theory.
10.00–12.00
Dag Westerståhl, Stockholm University
Carnap’s problem for intuitionistic propositional logic
Abstract: I will first give a brief background, with some examples, on ‘Carnap’s problem’: to what extent a consequence relation in a formal language fixes the meaning, relative to some given semantics, of the logical constants in that language. I then focus on intuitionistic propositional logic and show that it is ‘Carnap categorical’: the only interpretation of the connectives consistent with the usual intuitionistic consequence relation is the standard one. This holds relative to most well-known semantics with respect to which intuitionistic logic is sound and complete; among them Kripke semantics, Beth semantics, Dragalin semantics, and topological semantics. It also holds for algebraic semantics, although categoricity in that case is different in kind from categoricity relative to possible worlds style semantics. This is joint work with Haotian Tong.
10.00–12.00
Evan Cavallo, Stockholm University
Observational Type Theories
Abstract: I'll give a survey of Altenkirch, McBride, and Swierstra's observational type theory (OTT) and its descendants. In contrast to intensional Martin-Löf type theory, where equality types inductively generated by definitional equality, the OTT type of equalities in a type A is defined by recursion on the structure of A. The idea is that two elements are equal when they have the same behavior under appropriate observations: pairs are equal when their components are equal, functions are equal when they take equal values on all arguments. Moreover, the equality type is proof-irrelevant. I'll introduce the original OTT as well as Sterling, Angiuli, and Gratzer's re-imagination of OTT inspired by cubical type theory, called XTT, and recent work of Pujet and Tabareau.
10.00–12.00
András Kovács, Eötvös Loránd University
Generalized universe hierarchies and first-class universe levels
Abstract: In type theories, universe hierarchies are commonly used to increase the expressive power of the theory while avoiding inconsistencies arising from size issues. There are numerous ways to specify universe hierarchies, and theories may differ in details of cumulativity, choice of universe levels, specification of type formers and eliminators, and available internal operations on levels. In the current work, we aim to provide a framework which covers a large part of the design space. First, we develop syntax and semantics for cumulative universe hierarchies, where levels may come from any set equipped with a transitive well-founded ordering. In the semantics, we show that induction-recursion can be used to model transfinite hierarchies, and also support lifting operations on type codes which strictly preserve type formers. Then, we consider a setup where universe levels are first-class types and subject to arbitrary internal reasoning. This generalizes the bounded polymorphism features of Coq and at the same time the internal level computations in Agda.
10.00–12.00
Taichi Uemura, Stockholm University
Homotopy type theory as an internal language of a diagram of ∞-logoses
Abstract:
*Homotopy type theory* is an internal language of an
*∞-logos* (aka ∞-topos). But ∞-logoses are often connected by
functors and natural transformations. Homotopy type theory is, at
first sight, not sufficiently rich to reason about such a *diagram*
of ∞-logoses, because the actions of functors and natural
transformations are not internalized. Extending homotopy type theory
with non-internal modalities could be one solution, but it would
cause coherence problems for not only ∞-logoses but also functors
and natural transformations.
In this talk, we consider using *plain* homotopy type theory in some
way to reason about a diagram of ∞-logoses. We show that some kind
of diagram of ∞-logoses is reconstructed internally to its *oplax
limit* via *internal modalities*. Then plain homotopy type theory as
an internal language of the oplax limit can be used for reasoning
about the original diagram.
The first half of the talk will be an introduction to modalities in
homotopy type theory (Rijke, Shulman, and Spitters 2020
https://doi.org/10.23638/LMCS-16(1:2)2020). In the second half, I
will explain what kind of diagrams of ∞-logoses can be internally
expressed using modalities.
A short note is at
https://uemurax.github.io/pdfs/hott-uf-2022-notes.pdf.
11.00–12.00
Maximilian Doré, University of Oxford
Searching for Kan fillers with poset maps
Abstract: A central reasoning principle in cubical type theories is the notion Kan composition: In order to construct a filler with a certain boundary, one constructs a higher-dimensional box whose open side has the boundary under question. Since types in cubical type theories are Kan complexes, we will then have a term which acts as Kan composition of that box. We explore this reasoning principle from the point of view of computational logic and present strategies to search for boxes systematically. Using constraint satisfaction, we can solve most examples in lower dimensions. In higher dimensions, the number of degeneracies increases superexponentially. We present work in progress which uses the correspondence of degeneracies of De Morgan cubes with poset maps to represent the search space efficiently. This opens up the possibility to also search for boxes in higher dimensions.
10.00–12.00
Peter LeFanu Lumsdaine, Stockholm University
Quine’s set theory NF and relatives
Abstract:
This talk will be an introduction to Quine’s remarkable system NF, a set theory with a universal set. It has a very simple axiomatisation – extensionality, plus stratified comprehension – with powerful and subtle consequences. The world of NF is in many ways natural and idiomatic as a foundational setting, but very foreign from a ZF-acclimatised point of view.
A long-standing question is (or was) the consistency of NF. For the slightly variant NFU (NF with atoms) it is easy to exhibit models; but consistency of NF itself has long been elusive, until a recent proof by Randall Holmes – originally very technical and not widely accepted, but recently significantly simplified.
In this talk, I will briefly introduce NF, along with several variants and related systems, including NFU, TST, and Holmes’ TTT, and discuss their comparisons and model constructions. The seminar is partly intended as background for a possible future seminar on Holmes’ proof of consistency of NF.
10.00–12.00
Benedikt Ahrens, Delft University of Technology
The Univalence Principle
Abstract:
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk’s completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences.
Our work builds on Makkai’s First-Order Logic with Dependent Sorts, but is expressed in Voevodsky’s Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.
10.00–12.00
Steve Awodey, Carnegie Mellon University
A remark on Hoffman-Streicher universes
Abstract:
We have another look at the construction by Hofmann and Streicher [1] of a semantic universe El —> U for the interpretation of Martin-Löf type theory in a presheaf category [C^op, Set]. It turns out that El —> U can be described as the “categorical nerve” of the classifier Set* —> Set for discrete fibrations in Cat, where the nerve is the right adjoint in an apparently unnoticed adjunction,
int -| nerve : Cat —> [C^op, Set],
the left adjoint of which is the well-known “Grothendieck construction” taking a presheaf P : C^op —> Set to its category of elements int_C P .
[1] Lifting Grothendieck Universes, Martin Hofmann and Thomas Streicher, 1997 (unpublished).
10.00–12.00
Felix Cherubini, Chalmers University of Technology
Formalization of synthetic geometry
Abstract: With this talk, I would like to provide an overview of past and ongoing efforts to formalize parts of modern pure mathematics in (modal) homotopy type theory. The general idea is to use type theories as internal languages of toposes, which sometimes requires modalities to introduce relations of toposes into type theory. While it is not known, if there is a cubical type theory that admits interpretation in arbitrary toposes, those type theories are still interesting, since they provide at least some means of checking arguments involving more complicated higher inductive types. I will focus on more recent efforts to make a formalization of synthetic algebraic geometry possible with the cubical agda library.
10.00–12.00
Ivan di Liberti, Stockholm University
Bi-accessible and birepresentable 2-categories (part 2)
Abstract:
This continues from the introduction to presentable (1-)categories given last week.
We develop a 2-dimensional version of accessibility and presentability compatible with the formalism of flat pseudofunctors. First we give prerequisites on the different notions of 2- dimensional colimits, filteredness and cofinality; in particular we show that σ-filteredness and bifilteredness are actually equivalent in practice for our purposes. Then, we define bi-accessible and bipresentable 2-categories in terms of bicompact objects and bifiltered bicolimits. We then characterize them as categories of flat pseudofunctors. We also prove a bi-accessible right bi-adjoint functor theorem and deduce a 2-dimensional Gabriel-Ulmer duality relating small bilex 2-categories and finitely bipresentable 2-categories. Finally, we show that 2-categories of pseudo-algebras of finitary 2-monads on Cat are finitely bipresentable, which in particular captures the case of Lex, the 2-category of small lex categories. Invoking the technology of lex-colimits, we prove further that several 2-categories arising in categorical logic (Reg, Ex, Coh, Ext, Adh, Pretop) are also finitely bipresentable.
10.00–12.00
Ivan di Liberti, Stockholm University
Bi-accessible and birepresentable 2-categories
Abstract: We develop a 2-dimensional version of accessibility and presentability compatible with the formalism of flat pseudofunctors. First we give prerequisites on the different notions of 2- dimensional colimits, filteredness and cofinality; in particular we show that σ-filteredness and bifilteredness are actually equivalent in practice for our purposes. Then, we define bi-accessible and bipresentable 2-categories in terms of bicompact objects and bifiltered bicolimits. We then characterize them as categories of flat pseudofunctors. We also prove a bi-accessible right bi-adjoint functor theorem and deduce a 2-dimensional Gabriel-Ulmer duality relating small bilex 2-categories and finitely bipresentable 2-categories. Finally, we show that 2-categories of pseudo-algebras of finitary 2-monads on Cat are finitely bipresentable, which in particular captures the case of Lex, the 2-category of small lex categories. Invoking the technology of lex-colimits, we prove further that several 2-categories arising in categorical logic (Reg, Ex, Coh, Ext, Adh, Pretop) are also finitely bipresentable.
10.00–12.00
Thomas Lamiaux, Stockholm University
Univalent relational parametricity
Abstract:
The introduction of the axiom of Univalence gave content to the phrase "we identity isomorphic structure". Then it feels natural that if one proves a result on A which is equivalent to B then it also stands for B. However this is not automatic in HoTT\UF and requires a predicate P. It is technically possible in Cubical Agda, yet it is not trivial and can get quite involved. The seminar is about Univalent Relational Parametricity, which is a mixture of both Parametricity and Univalence that enables automatic transport of proofs.
During the first hour :
- The first part of the seminar will be an introduction on parametricity.
- The second will discuss the different ways to transport proofs and why this fails to be automated.
Focusing on the anticipation problemen and the computation problem.
The second hour and third part will be about the Univalent Relational Parametricity.
- Explaining Univalent Parametricity for CComega and explaining how it solves the anticipation and computation problem
- Explaining Univalent Relational Parametricity and why it is much better setting by just a twist in the definition
- Explaining how to extend Univalent Relational Parametricity to inductive types (nat, list ...) and to indexed inductive types (eq, vec...). Thus doing it for a great part of Coq.
10.00–12.00
Anders Lundstedt, Stockholm University
Natural induction—a model-theoretic study?
Abstract:
I present various notions of *inductiveness*—the original notion is due to Hetzl and Wong (2018). When suitably formulated, a *non-inductiveness* statement provides a precise and sensible sense in which a corresponding statement about the natural numbers is unprovable by straightforward induction. Thus by proving a suitable non-inductiveness result, one may show, in a precise and sensible manner sense, that some fact about the natural numbers is unprovable by straightforward induction.
I discuss the conceptual issue of how to formulate suitable non-inductiveness statements—where by ‘suitable’ I mainly mean formulations that actually provide the ‘sensible’ in my use of ‘precise and sensible sense’ above. Then I present techniques for proving non-inductiveness results: these are based on constructing certain kinds of non-standard models of first-order arithmetic.
I conclude by stating some non-inductiveness results that I have proved and some non-inductiveness conjectures that I hope to prove. If the conjectures turn out provable in the way I hope and believe, then that would perhaps justify removing the question mark from the ambitiously sounding paraphrase that is the title of this talk.
REFERENCES
- Hetzl, Stefan, and Tin Lok Wong (2018): Some observations on the logical foundations of inductive theorem proving. In: Logical Methods in Computer Science 13(4), pp. 1–26. (Corrected version of paper originally published Nov 16, 2017.)
- My research page
https://anderslundstedt.com/research/
has some very outdated material. Perhaps some new material will appear there in time before the talk.
10.00–12.00
Anders Lundstedt, Stockholm University
Imprecise thoughts entertained in mathematical practice and the special case of unprovability by straightforward induction
Abstract:
Mathematical definitions, results and proofs are almost always
precisely formulated (modulo details left for readers). On the other
hand, when mathematicians talk or think about definitions, results and
proofs, their formulations are not always precise.
(1) Mathematicians sometimes entertain thoughts to the effect that a
certain proof uses this or that method—while not always having a
precise and sensible meaning in mind for ‘this proof uses this or that
method’.
(2) Mathematicians sometimes talk about new proofs of already
established results—while not always being precise in what sensible
sense the new proof indeed ought to qualify as new.
(3) Mathematicians sometimes claim that this or that fact's
provability requires a certain “idea”—for example, a lemma or a
certain kind of construction.
(4) Mathematicians sometimes use the predicates ‘natural’ and
‘unnatural’ in intuitive but imprecise ways—as in, for example,
something like “that is a very unnatural proof”.
(5) In addition to examples (1)–(4), I have observed some hostility
among some mathematicians towards imprecisely phrased questions
regarding mathematical matters. Perhaps this is just me being biased
due to my frustration with MathOverflow closing some more or less
imprecise questions that I from time to time find interesting and
would like to see discussed.
This talk should be quite accessible. The plan is as follows:
- to briefly tell the story of how I first got interested in the
problem of making precise and sensible sense of imprecise things
thoughts entertained in mathematical practice;
- give some real-world examples falling under one or more of (1)–(5)
above, and for each briefly discuss whether it would be worth to try
to find a precise and sensible formulation; and
- in preparation for my talk at next week's seminar—and in particular
for its connection with (3)–(5) above—conclude with an introduction to
my work on *non-straightforward* induction proofs, going into some
technical details if time permits.
(“Non-straightforward” induction proofs are more often called
something like “proofs by generalizing the statement to prove”, but as
Eric Johannesson and I have shown, there are cases where “induction on
the statement itself” provably does not work, while—perhaps
surprisingly—an induction proof of a less general statement, or of a
weaker or incomparable statement, succeeds and gives the desired
statement as an immediate consequence.)
REFERENCES
- Hetzl, Stefan, and Tin Lok Wong (2018): Some observations on the
logical foundations of inductive theorem proving. In: Logical Methods in
Computer Science 13(4), pp. 1–26. (Corrected version of paper
originally published Nov 16, 2017.)
My research page
https://anderslundstedt.com/research/
has some material, but it is very outdated. Hopefully very soon I will
upload at least some of the following:
- Lundstedt, Anders (2022): Non-straightforward induction proofs and
the comparative strength of inductive solutions. Revised manuscript
for the presentation at the online seminar of the Computational Logic
group of the Institute of Discrete Mathematics and Geometry, TU Wien,
May 12, 2021.
- Lundstedt, Anders (2022): Some non-inductive formulas. Manuscript in
preparation.
- Lundstedt, Anders, and Eric Johannesson (2022): Comparing inductive
solutions. Manuscript in preparation.
10.00–12.00
Brandon Doherty, Stockholm University
Constructing connections in fibrant cubical sets
Abstract: Via the cubical Joyal model structure, (infinity,1)-categories may be modeled as cubical sets with connections having fillers for specified open boxes. Likewise, marked cubical sets with connections model (infinity,n)-categories for arbitrary n, via the comical model structures. In fact, these model structures may be defined in the presence of only faces and degeneracies, but previous proofs of their Quillen equivalence with established simplicial models made use of connections in an essential way. In this talk I will discuss a method by which model structures on cubical sets lacking connections may be shown to be Quillen equivalent to those with connections, using combinatorial techniques which allow the construction of connections in their fibrant objects via open-box filling.
10.00–12.00
Axel Ljungström, Stockholm University
The Fourth Homotopy Group of the 3-Sphere Is Z/2Z: A Complete(ly Formalised) Proof
Abstract: In his PhD thesis, Guillaume Brunerie proved, in Homotopy Type Theory, that the fourth homotopy group of the 3-sphere is isomorphic to Z/2Z. Despite being one of the most ambitious pieces of work in our field so far, Brunerie's proof has some relatively serious gaps. These gaps have, until recently, stood in the way of a fully formalised proof of the theorem in question. In this talk, I will give an overview of Brunerie's proof, tell you where the gaps are and, most importantly, tell you how to work around them (jww Anders Mörtberg).
10.00–12.00
Taichi Uemura, Stockholm University
Higher dimensional normalzation
Abstract:
We develop a normalization technique for the initial
space-valued model of a type theory. A consequence is that the
initial space-valued model coincides with the initial set-valued
model of the type theory, which allows us to interpret the type
theory in higher dimensional structures.
In the talk, we first review recent development of synthetic
normalization proof such as [1--3] and then discuss how to
generalize it to the higher dimensional setting.
[1] J. Sterling and C. Angiuli. Normalization for cubical type theory.
LICS 2021. doi:10.1109/LICS52264.2021.9470719
[2] D. Gratzer. Normalization for multimodal type theory.
https://arxiv.org/abs/2106.01414
[3] R. Bocquet, A. Kaposi, and C. Sattler. Relative induction principles for type theories.
https://arxiv.org/abs/2102.11649
10.00–12.00
Peter LeFanu Lumsdaine, Stockholm University
Setoids, e-categories, and saturation
Abstract: Setoids are strongly linked with constructive and computational mathematics, and often seen as outside classical mathematical practice. However, in the univalent development of category theory, setoids appear very naturally as part of the picture; and this leads to a precise and very close analogy between the use of setoids in constructive mathematics, and of categories in classical mathematics.
10.00–12.00
Ivan di Liberti, Stockholm University
Context, Judgement, Deduction
Abstract: We introduce judgemental theories and their calculi as a general framework to present and study deductive systems. As an exemplification of their expressivity, we recover type theory and proof theory as special kinds of judgemental theories. Our analysis sheds light on both the topics, providing a new point of view. In the case of type theory, we provide an abstract definition of type constructor featuring the usual formation, introduction, elimination and computation rules. In proof theory we offer a deep analysis of structural rules, demystifying some of their properties, and putting them into context. We finish the paper discussing the internal logic of a topos, a predicative topos, an elementary $2$-topos et similia, and show how these can be organized in judgemental theories. Based on a joint work with Greta Coraglia: https://arxiv.org/abs/2111.09438
10.00–12.00
Evan Cavallo, Stockholm University
Quillen model structures from models of cubical type theory, part 2
10.00–12.00
Evan Cavallo, Stockholm University
Quillen model structures from models of cubical type theory
10.00–12.00
Taichi Uemura, Stockholm University
∞-type theories and internal language problems
Abstract: We continue to prove Kapulkin and Lumsdaine's conjecture that the dependent type theory with intensional identity types gives internal languages for ∞-categories with finite limits. Last time we reviewed their conjecture, introduced the notion of ∞-type theory, and reformulated their conjecture in terms of ∞-type theories. This week we look at the technical core of the proof.
10.00–12.00
Karl Palmskog, KTH Royal Institute of Technology
Fast checking of Coq proofs, in theory and practice
Abstract: Large-scale Coq verification projects contain many proofs that must be checked at each new revision, e.g., when new lemmas are added and existing lemma statements and proofs are modified. This process of regression proving can be time consuming, which negatively impacts user productivity. In this talk, I will give an overview of the currently available techniques and tools for improving proof checking times in evolving Coq code and what we know about their efficacy from empirical evaluation on projects such as UniMath. I will focus on two core techniques: proof selection and proof parallelization. In proof selection, we attempt to avoid checking proofs that are unaffected by a change, and in proof parallelization, we leverage multi-core hardware on independently checkable proofs. Under certain conditions and assumptions that will be described in the talk, a combination of fine-grained selection and parallelization can give tenfold speedups over sequential checking of whole projects from scratch. Moreover, to increase trustworthiness, the proof selection technique itself has been formalized in Coq and proved sound.
10.00–12.00
Max Zeuner, Stockholm University
Pre-integration spaces in predicative Bishop-Cheng measure theory
Abstract: Building on a previous talk on the relationship between the classical theory of Daniell-spaces and integration spaces in the constructive Bishop-Cheng measure theory, we proceed to show how we can use set-indexed families to obtain a notion of pre-integration spaces and define the L^1-completion of such a pre-integration space, working entirely predicatively within constructive Bishop-style mathematics. This is j.w.w. Iosif Petrakis.
13.30–15.30
Brandon Doherty, Stockholm University
Cubical models of higher categories
Abstract: We describe a new model structure on the category of cubical sets with connections whose cofibrations are the monomorphisms and whose fibrant objects are defined by the right lifting property with respect to inner open boxes, the cubical analogue of inner horns. We discuss the proof that this model structure is Quillen equivalent to the Joyal model structure on simplicial sets via the triangulation functor, and a new theory of cones in cubical sets which is used in this proof. We also introduce the homotopy category and mapping spaces of a fibrant cubical set, and characterize weak equivalences between fibrant cubical sets in terms of these concepts. This talk is based on joint work with Chris Kapulkin, Zachery Lindsey, and Christian Sattler, arXiv:2005.04853.
10.00–12.00
Maximilian Doré, University of Oxford
Discrete Morse theory in Cubical Agda
Abstract: We will sketch how the main result of Discrete Morse theory, which states that it is possible to reduce large simplicial complexes to smaller CW complexes with the same homotopy type following a number of prescribed Whitehead collapses, can be expressed and formalized in Cubical Agda. We aim to explicitly compute the smaller complex and, by lifting the proof of equivalence to an equality with univalence, justify the correctness of any program using the smaller instead of the larger complex when computing, e.g., homology.
Memorial conference for Erik Palmgren — conference website
(Originally scheduled for Thu 7 – Fri 8 May; postponed due to Covid-19.)10.00–12.00
Max Zeuner, Stockholm University
A Cubical Approach to the Structure Identity Principle
Abstract:
The structure identity principle (SIP) is an informal principle, which asserts that reasoning about mathematical structures is invariant under isomorphisms of such structures. This can be made precise in HoTT/UF and formalized versions of the SIP have been proved for large classes of mathematical structures. We will discuss a version of the SIP that can be found in the lecture notes of Martín Escardó and our work can be seen as a reformulation of it in cubical type theory. By reformulating the SIP cubically some of the key proofs become more direct than in HoTT/UF, and furthermore, the cubical SIP lets us transport programs and proofs between isomorphic structures without sacrificing the computational content of the transported programs and proofs. We will then discuss a few examples to demonstrate how the cubical SIP is applied to actual instances of structures in mathematics and computer science.
(Joint work with Anders Mörtberg.)
10.00–12.00
Anders Mörtberg
Constructive Presheaf Models of HoTT/UF
Abstract: In recent years a variety of constructive presheaf models of Homotopy Type Theory and Univalent Foundations have been found. I will give an overview of these models and discuss some of the ideas that go into constructing them. A key idea of Ian Orton and Andrew Pitts is to axiomatize the models in the internal language of the presheaf topos and a variety of axiomatizations leading to different models have been found. These axioms are satisfied by any presheaf category where the base category has finite products and the interval object is representable, in particular by various cubical set categories. The talk will closely follow a recent survey article of Thierry Coquand titled “A survey of constructive presheaf models of univalence” that can be found at: doi:10.1145/3242953.3242962
10.00–12.00
Nima Rasekh, EPFL
An example of an elementary higher topos that is not a Grothendieck higher topos
Abstract:
The theory of Grothendieck higher toposes has been developed quite extensively, which has led to many interesting examples, from sheaves on smooth schemes to 1-excisive functors.
On the other hand, the generalization of Grothendieck higher toposes, namely elementary higher toposes, is a recent development and as of now lacked interesting examples that would demonstrate the additional theoretical strength.
The goal of this talk is to give a class of examples of elementary higher toposes that are not Grothendieck higher toposes, via the filter quotient construction. If time permits, we will focus on one example and show how its non-standard natural number object leads to non-standard truncation levels.
10.00–12.00
Anders Mörtberg
Programming and proving with higher inductive types in Cubical Agda, Part II
Abstract: This will be a continuation of last week’s seminar.
10.00–12.00
Anders Mörtberg
Programming and proving with higher inductive types in Cubical Agda
Abstract: The recently developed cubical mode of Agda allows the user to define their own higher inductive types (HITs). The user can then also conveniently program and reason about these using pattern-matching. I will show a variety of examples, taken from computer science, logic, algebra and synthetic homotopy theory, that we have developed in Cubical Agda. Working in a system with native support for HITs has many benefits compared to working axiomatically. For example, the proof of the 3x3 lemma for pushouts is less than 200 lines in Cubical Agda which can be compared to the 3000 line proof in HoTT-Agda with postulated HITs.
10.00–12.00
Anja Petković, University of Ljubljana
Andromeda 2.0
Abstract: Andromeda 2.0 is a proof assistant in development in which the user can specify a general type theory (in the sense of Bauer, Haselwarter, and Lumsdaine). I will present the main features it supports, how one operates with judgements, defines the rules of the theory, derives the congruence rules etc. We will illustrate these on some standard examples of type formers like dependent sums and products. This is joint work with Andrej Bauer and Philipp G. Haselwarter.
10.00–12.00, Rum 406
Colin Zwanziger, Carnegie Mellon University
Towards CwF semantics for modal dependent type theory
Abstract: Modal logic may be modeled using Cartesian functors and geometric morphisms between toposes (Reyes and Zolfaghari 1991, Zwanziger 2017). Analogously, modal dependent type theory may be modeled using weak morphisms and "geometric morphisms" between categories with families (CwFs), at least in a few fundamental cases (Birkedal et al. 2018, Zwanziger 2019). I illustrate one of these, giving an interpretation for an adjoint dependent type theory (cf. Krishnaswami et al. 2015) using a geometric morphism of CwFs.
10.00–12.00
Benno van den Berg, University of Amsterdam
Uniform Kan fibrations in simplicial sets
Abstract: An important question in homotopy type theory is whether the existence of a model of univalent type theory in simplicial sets (and a model structure) can be proven constructively (say, in CZF with some inaccessibles). One approach would be to take the usual definition of a (trivial) Kan fibration as one's starting point and see how far one gets: this is the approach followed by Henry, Gambino, Szumilo and Sattler in recent work. It turns out that you can get quite far, but some issues remain (especially around the interpretation of Pi-types and coherence). Together with Eric Faber, I am pursuing a different approach in which we add uniformity conditions to the notion of a Kan fibration (as in the cubical sets model). The idea is that classically these conditions can always be satisfied, but not necessarily constructively. This has also been tried by Gambino and Sattler in earlier work, but in our view there are quite a few conditions missing in their definition of a uniform Kan fibration. In this talk, I will try to explain what our definition is, why we believe our definition is better (the idea is that we can prove, constructively, that it is "local"), and how far we are right now.
10.00–12.00
Peter LeFanu Lumsdaine
Essentially algebraic theories and Gabriel–Ulmer duality II
Abstract:
This will be a continuation of my talk from October 16.
Gabriel–Ulmer duality gives a tight connection between essentially algebraic theories and their categories of models. I will give an exposition of this duality, with an emphasis on its concrete logical interpretation and applications.
10.00–12.00
Martijn den Besten, University of Amsterdam
Coherence for bicategories and bigroupoids
Abstract: This talk is loosely based on [1], in which I prove and apply a coherence theorem for bigroupoids. During the talk, I will briefly sketch the main proof idea for the coherence theorem for bigroupoids and I will present, in some detail, the well-known proof of the coherence theorem for bicategories using the bicategorical Yoneda lemma.
10.00–12.00
Peter LeFanu Lumsdaine
Essentially algebraic theories and Gabriel–Ulmer duality
Abstract: Gabriel–Ulmer duality gives a tight connection between essentially algebraic theories and their categories of models. I will give an exposition of this duality, with an emphasis on its concrete logical interpretation and applications.
14.30–16.30
Paige North, Ohio State University
Two-sided weak factorization systems
Abstract: In this talk, I’ll describe intended semantics for directed type theory. We generalize the two-sided fibrations of Street to obtain a notion of two-sided weak factorization systems: structure on a category which consists of two compatible weak factorization systems. These correspond to a notion of directed path object. The long-term goal is to use the behavior of these directed path objects to reverse-engineer a directed identity type.
10.00–12.00
Benedikt Ahrens, University of Birmingham
Initial semantics for lambda calculi
Abstract TBA.
10.00–12.00
Douglas S. Bridges, University of Canterbury, Christchurch, NZ
Apartness on Lattices
Abstract: I shall present the outlines of a lifting of the theory of apartness between sets to a more general, pointfree (pointless?) theory of apartness on certain lattices. The framework is Bishop’s constructive mathematics.
10.00–12.00, Hus 5, Rum 16 (Note nonstandard day)
Erik Darpö Nagoya University
On constructive semigroup theory
Abstract: In this talk, I shall speak about some basic notions of semigroup theory from a constructive viewpoint. The focus will be on the concept of apartness (i.e., inequality) in sets and semigroups, and how the presence of an apartness relation leads to additional considerations compared with the classical situation.
Conference Mathematical Logic and Constructivity (MLoC) 2019 — conference website
10.00–12.00
Guillaume Brunerie
π₄(S³) in homotopy type theory, part II
Abstract: This is a continuation of the seminar of May 29.
10.00–12.00
Anna Montaruli
A constructive approach to the Freyd-Mitchell Embedding Theorem
Abstract:
The Freyd–Mitchell Embedding Theorem states that every abelian category with some extra properties can be embedded into a category of modules over a certain ring. This result is constructively suspicious, and its proof seems to be non-constructive in many parts.
After a brief introduction on abelian categories, I'll present the proof of the theorem, pointing out the parts in which non-constructive tools are used, and showing some small counterexamples.
The talk, based on joint work with Erik Palmgren, aims to present a status report on the project.
10.00–12.00
Guillaume Brunerie
π₄(S³) in homotopy type theory
Abstract: In this talk I will present the main result of my PhD thesis, namely that π₄(S³) is isomorphic to Z/2Z in homotopy type theory. In order to translate this well known result from classical homotopy theory to homotopy type theory, several common constructions of homotopy theory (like the James construction, the Hopf invariant, the Gysin sequence) have to be redefined in a homotopy-invariant way using tools from homotopy type theory like higher inductive types and univalence. I will aim to make this talk accessible to both logicians and topologists.
10.00–12.00
Antje Rumberg
Pruning the Tree of Possibilities: Axiomatizability Results for Transition Semantics
Abstract:
In my talk, I will give an overview of transition semantics for branching time, which I have developed in my dissertation, and sketch some axiomatizability results, drawing on joint work with Alberto Zanardo.
The theory of branching time, pioneered by Prior, depicts the future as genuinely open. The picture is that of a tree, whose branches represent possibilities for the future. The distinctive feature of transition semantics is that it provides a local approach to branching time: building on local future possibilities, viz. transitions, rather than on complete possible courses of events, it allows for a fine-grained, dynamic picture of the interrelation of modality and time, and it generalizes and extends extant accounts.
In the first part of my talk, I will motivate the basic idea underlying transition semantics and introduce the overall framework. It will become apparent that the semantics is set-theoretically rather complex. In the second part, I will then show that the set-theoretic complexity can be evaded – owing to the notion of a pruning. Based on this notion, I will provide a class of first-order definable Kripke structures that preserves validity, which naturally leads to axiomatizability results.
10.00–12.00
Sebastian Enqvist
Disjunctive bases II
Abstract: This is a sequel to the previous seminar of February 20.
10.00–12.00
Joseph Helfer, Stanford University
First-order homotopical logic
Abstract: Our story begins with the observation that the Voevodsky–Awodey–Warren–Kapulkin–Lumsdaine homotopical semantics for type theory can also be used to give a very simple semantics for (intuitionistic) first-order logic. We will describe a “functorial” formulation of these semantics using the framework of structured Grothendieck fibrations, by showing that the fibration obtained by taking the fiberwise-homotopy-category of the codomain fibration over a (suitable) model category C has the structure needed to interpret intuitionistic first-order logic. We will then describe an abstract result about such structured fibrations which implies a “homotopy-invariance” property for the homotopical semantics. To do this, we must make sense of the notion “homotopy-equivalent structures” in the general context of the “fibrational” semantics. This leads us to describe a 2-categorical structure which is automatically present on the base category of a fibration (satisfying certain mild assumptions) — the 2-cells between f and g being “proofs (in the sense of the fibration) that f and g are equal — which in the case of interest recovers the usual 2-category of spaces.
10.00–12.00
Eric Finster
Left Exact Modalities in Type Theory
Abstract:
In ordinary topos theory, one can encode the notion of a subtopos as a Lawvere-Tierney topology on the sub-object classifier. Viewing homotopy type theory as an internal language, this time for higher toposes, the natural replacement for such a topology is a modality on the universe of types. But whereas the localization associated to a Lawvere-Tierney topology always preserves finite limits and thus determines a subtopos, this fails to be the case in general in type theory (the n-trucation modalities provide a simple class of counterexamples). Those modalities which do in fact preserve finite limits, and thus determine a subtopos, are called left exact.
In this talk, I will discuss the problem of lex modalities in type theory and exhibit a criterion which allows us to detect when modalities do indeed generate sub-toposes, as well provides us with tools to generate such modalities. Time permitting, I will explain how every left exact modality generates and infinite tower of associated modalities and describe some properties of this tower.
10.00–12.00
Håkon Gylterud, University of Bergen
Quote operations on λ-calculus and type theory
Abstract: Going back to Gödel, we know that many formal languages have the ability to represent their own syntax. The operation which turns an expression into its internal representation is called quoting. For programming languages, one can also ask if they can internally represent their own evaluation function. Work by Brown and Palsberg[0] shows that this is even possible to some extent for strongly normalizing languages.
Quoting is usually a meta-theoretical operation. However, some programming languages, such as LISP or Scheme, have this as an internal operation in the language. In this talk I will present extensions of λ-calculus and type theory with internal quoting operations. They differ from the LISP or Scheme equivalents by being confluent while allowing reductions under the quote.
The motivation for this work is to study how Church’s thesis, which states that every function is computable, can be seen as a quoting operation with extra properties. We will discuss how this statement can be internalised and demonstrated in an extension of intensional Martin-Löf type theory.
[0]: Breaking through the Normalization Barrier: A Self-interpreter for F-omega, M. Brown and J. Palsberg, Proceedings of POPL'16.
10.00–12.00
Chaitanya Leena Subramaniam, Université Paris Diderot
Nerves, monads with arities, and theories for ∞-categories and ∞-operads
Abstract: Categories of algebras often have a well understood nerve functor which is an embedding into a presheaf category---familiar examples are the embedding of Cat into Psh(Δ), of Operad into Psh(Ω), of Set into Psh(Fin), and of T-Alg into Psh(Kleisli_T).
The theory of monads with arities permits the study of free constructions on algebras at the level of their nerves---examples of such are the free-category construction on a graph and the free-operad construction on a collection. In addition, when the nerve functor is the right adjoint to a reflexive localisation of a locally presentable category (almost all of our previous examples), this theory admits a particularly nice description.
Similarly, higher categories of higher algebraic structures are often concretely dealt with via nerve functors---the nerve of an ∞-category is a simplicial space; that of an ∞-operad is a dendroidal space. Indeed, the theory of monads with arities makes sense in the ∞-world.
This (largely expository) talk will introduce monads with arities and their relationship to localisations of locally presentable categories. This will then be generalised to locally presentable ∞-categories, and formulated using combinatorial simplicial model categories and left Bousfield localisation. The running examples will be the free-category monad on Graph, the free-operad monad on Coll (the category of coloured, symmetric collections), and their ∞-categorical generalisations.
References:
10.00–12.00
Hugo Moeneclaey
Monoids up to coherent homotopy in two-level type theory
Abstract : When defining a monoid structure on an arbitrary type in HoTT, one should require a multiplication that is not only homotopy-associative, but also has an infinite tower of higher homotopies. For example in dimension two one should have a condition similar to Mac Lane’s pentagon for monoidal categories. We call such a monoid a monoid up to coherent homotopy. The goal of my internship in Stockholm was to formalize them in Agda. It is well-known that infinite towers of homotopies are hard to handle in plain HoTT, so we postulate a variant of two-level type theory, with a strict equality and an interval type. Then we adapt the set-theoretical treatment of monoids up to coherent homotopy using operads as presented by Clemens Berger and Ieke Moerdijk [1,2].
Our main results are:
10.00–12.00
Peter LeFanu Lumsdaine
Small-object arguments: algebraic, fat, enriched, oh my! (expository)
Abstract: The small object argument is a versatile tool, originally introduced by Quillen for abstract homotopy theory, and since then adapted for a wide range applications in algebraic topology, logic, and pretty anywhere else that category theory is significantly used.
In this mainly expository talk, I’ll recall several versions of the small object argument, including at least
10.00–12.00
Peter LeFanu Lumsdaine
Basic metatheorems for general type theories
Abstract: I will recall the definition of general type theories I presented in October, and look at the proofs of basic fitness-for-purpose metathorems for them — uniqueness of typing, admissibility of substitution, derivability of presuppositions, and so on. In particular, I’ll look at where the proofs of these in wider generality need to differ from their proofs for individual type theories. (Joint work with Andrej Bauer, Philipp Haselwarter)
10.00–12.00
Per Martin-Löf
Logic and ethics
Abstract:
10.00–12.00
Sebastian Enqvist, Stockholm University
Disjunctive bases: a coalgebraic approach to normal forms in modal logic
Abstract:
I present the concept of a disjunctive basis, a generic framework for normal forms in modal logic based on coalgebra, and provide some illustrating examples. The presence of a disjunctive basis entails a number of good properties for a coalgebraic modal logic and its mu-calculus extension, in particular, a simulation theorem showing that every alternating automaton can be transformed into an equivalent nondeterministic one. This leads to a number of results: a Lyndon theorem for the full fixpoint logic, its fixpoint-free fragment and its one-step fragment, a Uniform Interpolation result, for both the full mu-calculus and its fixpoint-free fragment, and a Janin-Walukiewicz-style characterization theorem for the mu-calculus under slightly stronger assumptions. Furthermore, existence of a disjunctive basis is closed under some natural operations for modular construction of coalgebraic logics: sum, product and composition.
The talk is based on joint work with Yde Venema.
10.00–12.00
Andrej Bauer, University of Ljubljana
What is algebraic about algebraic effects and handlers?
Abstract: In this tutorial talk we draw an uninterrupted line of thought between algebra and computational effects. We begin on the mathematical side of things, by reviewing the classic notions of universal algebra: signatures, algebraic theories, and their models. We then generalize and adapt the theory so that it applies to computational effects. In the last step we replace traditional mathematical notation with one that is closer to programming languages.
Andrej Bauer, What is algebraic about algebraic effects and handlers? arXiv:1807.05923, 2018
10.00–12.00
Erik Palmgren
A setoid model of extensional Martin-Löf type theory in Agda
Abstract: We present details of an Agda formalization of a setoid model of Martin-Löf type theory with Pi, Sigma, extensional identity types, natural numbers and a universe à la Russell. A crucial ingredient is the use of Aczel’s type V of iterative sets as an extensional universe of setoids, which allows for a well-behaved interpretation of type equality.
11.30–17.15
3rd joint Göteborg–Stockholm type theory seminar, Chalmers University of Technology, EDIT building, room 8103.
Schedule:
10.00–12.00
Jacopo Emmenegger
W-types in setoids
Abstract: W-types are very general inductive types and, from a set-theoretic perspective, can be seen as representatives of well orders. Moerdijk and Palmgren identified a semantic analogue in initial algebras of polynomial endofunctors. Current arguments to obtain such initial algebras in categories of equivalence relations rely on assumptions like Uniqueness of Identity Proofs or on constructions that involve recursion into a universe. We present a new argument, verified in Coq, that instead uses a generalisation of W-types in the underlying type theory, known as dependent W-types. These type constructors endow the theory with enough expressive power to characterise maps obtained by initiality as those maps satisfying a certain recursive equation. In addition, not relying on any extensionality principle nor on existence of universes, this argument is valid in a fully intensional theory and it is suitable for being formulated in rather weak category-theoretic settings.
10.00–12.00
Chris Kapulkin, University of Western Ontario
Cubical sets and higher category theory
Abstract: I will report on the recent joint work with Voevodsky on using cubical sets to gain a better understanding of a number of constructions in higher category theory. This work is inspired by the use of cubical sets in Homotopy Type Theory by Coquand and his group.
10.00–12.00
Bahareh Afshari, University of Gothenburg
Nested sequents for fixed point modal logic
Abstract:
Modal logic provides an effective language for expressing properties of state-based systems. When equipped with operators that can test for infinite behaviour like looping and reachability, the logic becomes a powerful tool for specifying correctness of nonterminating reactive processes such as communication protocols and control systems. An elegant example of such a logic is the modal mu-calculus which extends basic modal logic by two quantifiers for defining inductive and co-inductive operators.
In this talk I will introduce the modal mu-calculus and present a complete proof system for it based on nested sequents. We will see how the proof system can be used to obtain a constructive proof of the finite model property and, time permitting, I will also explain how the framework lends itself to a sound and complete axiomatisation for the extension of mu-calculus with backward modalities.
10.00–12.00
Favonia, CAS Oslo
Normalization in Cubical Type Theory
Abstract:
Cubical type theory is the first known strategy to give constructive
meanings to new features introduced by homotopy type theory, including
univalence and higher inductive types. However, the new judgmental
structure complicates the usual story of normalization, which makes
efficient implementations challenging.
The fundamental problem is that we have to consider partial elements
under a theory of equations of dimensions, and a normal form may cease
to be normal under a different theory. In this talk, I will explain
our current attempts towards an updated account for cubical type
theory.
10.00–12.00
Peter LeFanu Lumsdaine
Initiality for a general class of type theories
Abstract: I will present a definition of a general class of dependent type theories, and sketch a proof of an initiality result for such theories. I will give some comparison with Guillaume Brunerie’s independent work on the same topic, presented in the seminar last month. If time allows, I will also present an ongoing formalisation of this work. (This is joint work with Andrej Bauer and Philipp Haselwarter.) This will to some extent recapitulate previous seminars I’ve given on this work, but will aim to be self-contained and comprehensive.
10.00–12.00
Anders Mörtberg
Cubical techniques in homotopy type theory and univalent foundations
Abstract: In recent years there has been a lot of progress on a variety of problems in homotopy type theory and univalent foundations using cubical techniques. This has for example resulted in multiple constructive justifications to Voevodsky’s univalence axiom, new models of higher inductive types and an analysis of the proof theoretic strength of the univalence axiom. Another interesting aspect of these developments is that we can design type theories inspired by these cubical models in which functional extensionality, univalence and higher inductive types are directly definable and hence has computational content. I will give an overview of these developments and discuss some current challenges and open problems.
10.00–12.00
Menno de Boer
The gluing construction for path categories
Abstract: Path Categories are a categorical semantics for homotopy type theory with propositional identity types. In this type theory, the judgmental equality in the elimination rules is replaced by propositional equality. This has some direct consequences when one deals with universal constructions like exponentials and natural numbers object: they will have a homotopic counterpart. Additionally, if one has an appropriate functor F between two such categories, it is possible to define a new path category GL(F), called the gluing category. During my master’s thesis I have studied this gluing category and specifically when it preserves these homotopy universal constructions. During my talk, I will first give a motivation for such gluing constructions, before I will introduce you to Path Categories. After this introduction, I will give the definitions of homotopy universal constructions and the gluing category, before ending with some of the results from my thesis regarding these constructions. I will assume basic knowledge of category theory and some intuitive understanding of type theory.
14.30–16.15, room 31, building 5. (Note nonstandard location!)
Floris van Doorn, Carnegie Mellon University/CAS Oslo
Towards spectral sequences for homology
Abstract: Homotopy type theory has lead to a new research area, synthetic homotopy theory, in which results in homotopy theory are stated and proven in type theory. Many advances have been made in doing cohomology theory in homotopy type theory, such as the Mayer–Vietoris sequence and the Serre and Atiyah–Hirzebruch spectral sequences for cohomology. The progress in homology theory is much slower. During this talk I will explain some difficulties in doing homology theory and talk about the work in progress to get the Serre and Atiyah–Hirzebruch spectral sequences for homology. Along the way, I will discuss the related project of the coherent associativity of the smash product. Some basic knowledge of homotopy type theory is assumed for this talk.
10.00–12.00
Guillaume Brunerie
A proof sketch for the initiality conjecture
Abstract:
The initiality conjecture states that given a type theory, the syntactic model forms an initial object in the category of models of this type theory.
This fact is often assumed to be obvious and is rarely proved in detail. For instance it is implicitly assumed in order to show that there is a canonical way to interpret the syntax of type theory in any given model. However, there are many technical details that need to be taken care of in the proof, and it is not even clear what the precise statement of the initiality conjecture is. What is a type theory? What is a model? What is the syntactic model?
This was particularly emphasized by Vladimir Voevodsky who couldn’t find any proof of the initiality conjecture in the literature that would apply to Martin-Löf type theory and allow for extensions like his resizing rules.
In this talk I will present work in progress on this problem. I will define a class of type theories general enough to allow for many variants of dependent type theory, and sketch the definition of the category of models, the definition of the syntactic model, and the proof of initiality.
10.00–12.00
Göran Sundholm, Leyden University
Intended interpretations and the choice of formal systems: Themes from Kreisel’s work on constructivist foundations
Abstract: In his lecture at the 1983 Salzburg Gödel Conference, Kreisel noted:
The occasion demands a topic that spans, if possible, Gödel’s working life. For me that singles out the area of intuitionistic logic.Mutatis mutandis the same applies to the present occasion and Kreisel. Accordingly, my talk deals with Kreisel’s thought on Constructivist Foundations that provided the setting for much of his most trenchant work, up to and including the period of Hochleistung, 1955–1975. Kreisel’s insightful Bucharest Question from LMPS 4
Was the (logical) language of the current intuitionistic systems obtained by uncritical transfer from languages which were, tacitly, understood classically?will be used to turn the tables on him with respect to four topics:
Time permitting, I also consider Kreisel’s much discussed Dictum, as formulated by Michael Dummett, and put on record Kreisel’s own views on this Dictum as given to me in 1978. Furthermore I hope to consider a suggestion of Hidé Ishiguro as to the identity of “Al Tajtelbaum, New York”, the winner of Miss Anscombe’s Analysis Problem No. 10 in Analysis 17, pp. 49–52.
10.00–12.00
Per Martin-Löf
Weyl’s attempted mediation between intuitionism and formalism
10.00–12.00
Peter LeFanu Lumsdaine
Projectivity in the free topos
Abstract: I will discuss some classic results on projectivity in the free topos — in proof-theoretic terms, existence properties for intuitionistic higher-order logic (IHOL). In particular, I will look at:
10.00–12.00
Jan Cedervall, Stockholm University
Para-consistent, doxastic hybrid logic
Abstract: In general choices are at least to some extent governed by expectations. While the world is consistent expectations about the world may be ambivalent or contain other para-consistencies. We hence argue that the normal Kripke axiom and necessitation are too strong for modelling expectations behind real-time choices where recovery from mistakes are impossible. Thus, weaker versions are suggested as a base for a para-consistent, doxastic hybrid logic, that still allows a relational semantics. Weaker axiom and the lack of full necessitation makes the logic deductively weaker. Model dynamics and logical induction are discussed, as ways to strengthen the weakened computational and concluding power.
10.00–12.00
Peter LeFanu Lumsdaine
Towards a general meta-theory of dependent type theories
Abstract: This talk is an update on work in progress with Andrej Bauer and Philipp Haselwarter, on formulating and formalising a general definition of dependent type theories which is:
Cancelled due to illness.
10.00–12.00
Jacopo Emmenegger
W-types in the setoid model
Abstract: A W-type is a very general inductive type, encompassing natural numbers and lists, for example. Moerdijk and Palmgren identified a semantic analogue in initial algebras of polynomial endofunctors.
We will report on current work in progress to obtain such initial algebras in the setoid model in intensional Martin-Löf type theory. In particular, we will present an idea which allows us to avoid the limitations of previous solutions to the problem, which make use of UIP or of recursion into a universe.
10.00–12.00
Johan Lindberg
Logical Spaces
Abstract: In this presentation we describe an ongoing project of giving a more explicitly logical proof of the Joyal–Tierney representation theorem for Grothendieck toposes.
A key aspect of our approach is the use of complete Heyting Algebra (cHA) valued sets instead of sheaves. One reason for pursuing this line of research is to further develop the constructive model theory for geometric and first-order intuitionistic logic with respect to cHA-valued sets, and to clearify its connections with more general topos-theoretic machinery.
This is joint work with Henrik Forssell.
10.00–12.00
Valentin Goranko, Stockholm University; Ruaan Kellerman, University of Pretoria
Towards model theory of trees generated by elementary classes of linear orders
Abstract:
This is an overview talk on an ongoing research project studying logical theories of classes of trees (as partial orders), also joint with Alberto Zanardo (University of Padova).
Given a class of linear order types C, several different classes of trees are naturally associated with C in terms of how the paths in those trees are related to the order types in C. In a previous work we have studied and completely determined the set-theoretic relationships between these classes of trees and between their corresponding first-order theories. We have also obtained some general and some specific results on axiomatizations of the first-order theories of some such classes of trees defined in terms of the generating class of linear orders C.
In this talk we present an overview of that work and will outline its extension to a more general model-theoretic study of classes of trees generated by elementary classes of linear orders. We will focus on the axiomatizations of their first-order theories, first-order definability and non-definability of paths and other special sets in such trees, and some structural properties of certain natural classes of trees. Besides some known results, we will present a number of open problems.
For this talk we will not presume any essential background beyond some basic knowledge on model theory of first-order logic.
11:30–18:00
2nd joint Stockholm–Göteborg type theory seminar, Kräftriket hus 5, rum 32.
Schedule:
Jesper Cockx, Chalmers University of Technology
Elaborating dependent (co)pattern matching
Abstract:
In a dependently typed language, we can guarantee correctness of our programs by providing formal proofs. To check these proofs, the typechecker elaborates our programs and proofs from the high-level surface language into a low level core. However, this core language is by nature hard to understand by mere humans, so how can we know we proved the right thing? In this paper we study this problem in particular for dependent copattern matching, a powerful language construct for writing programs and proofs by dependent case analysis and mixed induction/coinduction. A definition by copattern matching in the surface language consists of a list of equations called clauses that are elaborated to a series of case splits structured as a case tree, which can be further translated to primitive eliminators. This second step has gotten a lot of attention in previous work, but in comparison the first step has been mostly ignored so far.
We present a dependently typed core language with inductive datatypes, coinductive record types, an identity type, and defined symbols represented by well-typed case trees. We also present an elaboration algorithm translating definitions by dependent copattern matching to a case tree in this core language. To make sure the user of our language does not have to look at the generated case tree, we prove that elaboration preserves the first-match semantics of the clauses given by the user. Based on the ideas in this paper, we reimplemented the algorithm used by Agda to check left-hand sides of definitions by pattern matching. The new implementation is at the same time more general and less complex, and fixes a number of bugs and usability issues with the old implementation. Thus this paper brings us one step closer towards a formally verified implementation of a practical dependently typed language.
Jacopo Emmenegger, Stockholm University
The homotopy exact completion and properties of cartesian closure
Abstract: Carboni and Rosolini’s characterisation of (local) cartesian closure of exact completions E as a property of the projective objects P only holds if the projectives are closed under pullback. When considering the setoid construction in type theory, this requirement is equivalent to UIP. To overcome this problem, we introduced with Erik Palmgren a condition on P inspired by Aczel’s Fullness Axiom in CZF and showed that it implies the local cartesian closure of E. In a recently published paper, van den Berg and Moerdijk have described a new way to build an exact category Hex(C) out of a category with homotopical data C (a so-called path category).
We will briefly recall all the notions involved and discuss how van den Berg and Moerdijk’s argument for the local cartesian closure of Hex(C) relates to our categorical Fullness condition.
Thierry Coquand, Göteborg University
Presheaf models and combinatorial topology
Abstract:
One goal of combinatorial topology was to avoid set theoretic difficulties and to present
spaces not as a set of points but in a combinatorial way as a finite number of inter-related
abstract entities. This idea is expressed in an elegant way using the notion of presheaves
but it can be argued that the present way of doing this does not avoid set theoretic
complexities.
Using the fact that presheaves form a model of dependent type theory,
we explain various way to formulate some
homotopy extension property (equivalent to the Kan property in the case of simplicial sets).
This is then used to describe basic spaces (such as the sphere) and operations on spaces
(such as the suspension) in a constructive setting.
10.00–12.00
Simon Henry, Masaryk University, Brno
Constructive homotopy theory, Weak model structures and infinity groupoids in type theory
Abstract:
This talk will be about two closely related topics:
In the first part I will introduce a notion of “weak model structure”. It is a weakening of the notion of Quillen model structure, which still allows to carry most of usual homotopy theory. These weaker structure appear to be considerably easier to construct than Quillen model structures, so much so that it will be possible to get rather directly ‘weak’ analogue of most classical model structures, in constructive and even predicative mathematics. This includes things like the Quillen model structure on simplicial sets, the model structure for quasi-categories, chain complexes, cubical sets, dendroidal sets, the folk model structure on infinity category, and lots of other examples…
In the second part, I will present some new tools to construct and compare concrete models for the notion of infinity groupoids. These tools will have two interesting applications:
They allow to construct a new notion of infinity groupoids which:
10.00–12.00
Peter LeFanu Lumsdaine
Inverse diagram models of type theory, part 3
Abstract: I will revisit inverse diagram models of type theory, which I previously spoke about in the seminar last November. In particular, I will talk about how functors between inverse categories induce maps between their diagram CwA’s, and give the (rather fun) proof that a homotopy equivalence of inverse categories induces a local equivalence of diagram CwA’s.
As background, it will be helpful if you either have some recollection (possibly hazy) of my seminars last November, or else have viewed my online seminar from last Thursday in the HoTTEST series — slides and video to be posted shortly at http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html.
10.00–12.00, Hus 5, Sal 35 (note location!)
Erik Palmgren
Exploring generalized algebraic theories with the proof assistant Agda
Abstract:
Generalized algebraic theories (GATs) (Cartmell 1978, 1986) is a general form equational logic where the sorts (types) can depend on other sorts and terms, also, it allows for equations between sorts. GATs can serve as basis for categorical theories, and for type theory itself.
Most proof assistants do not allow for the introduction of arbitrary judgemental equalities as GATs do, since this would destroy decidability of type checking. In this talk we explore the possibility of to implement GATs as a term calculus in Agda, and the prospects of formalizing proofs of meta-theorems about GATs.
10.00–12.00
Douglas Bridges, University of Canterbury
Ishihara’s research in constructive analysis
Abstract: The aim of this talk is to present some of Ishihara’s fundamental contributions to Bishop-style constructive analysis, and their consequences. Among the areas discussed in the talk are:
10.00–12.00, Hus 6, Rum 16
Christian Espíndola
A categorical approach to infinite alternate quantifiers and completeness for game semantics
Abstract:
Infinite alternate quantifiers, also known as heterogeneous quantifiers, present a new type of quantification in infinitary logic whose interpretation is usually associated to infinite games. Takeuti considered a proof theory for heterogeneous quantifiers based on Gentzen sequents and including the axiom of determinacy, according to which in every game one of the players has a winning strategy.
We present here a categorical approach to heterogeneous quantifiers extending the presentation given for usual classical infinitary logic with homogeneous quantification, and provide an axiomatization within the system commonly used in categorical logic. We prove that under this axiomatization, set models in special types of structures that we call well-determined correspond precisely to infinitary Boolean set-valued functors from what we call an heterogeneous category, and using the theory of k-Grothendieck toposes we prove that our system is sound and complete for well-determined structures with the game semantics. We also discuss completeness in terms of models in heterogeneous toposes.
10.30–11.30, Hus 6, Sal 306 (note time + location!)
Douglas S. Bridges, University of Canterbury, Christchurch, New Zealand
Some Favourite Constructive Theorems of Mine
Abstract:
Retirement presents an ideal opportunity for reflection on one’s professional life. In this talk I reflect on my work in a number of areas of Bishop-style constructive mathematics (BISH)—that is, mathematics with intuitionistic logic and an appropriate set- or type-theoretic foundation.
The key feature of BISH is its systematic use of intuitionistic logic, which captures formally the essence of the constructive proof-development process and enables one to work in the normal style of, for example, an analyst or an algebraist. Every proof in BISH is essentially an algorithm, and the proof itself can be read as proof that the algorithm contained in it meets its specifications. (Several computer-science groups have extracted and implemented those algorithms for parts of analysis.)
Among the areas discussed in the talk are:
10.00–12.00
Anders Lundstedt, Dept. of Philosophy, Stockholm University
TBA
10.00–12.00, Hus 6, Sal 306 (Cramér-Rum)
Norihiro Yamada, University of Oxford
Game Semantics of Martin-Löf Type Theory
Abstract: In this talk, I present my work on game semantics of Martin-Löf Type Theory (MLTT).
Game semantics has been a highly successful approach to semantics of logic (and computation), which interprets proofs as “dialogical arguments” of a prover mathematician against a refuter mathematician in a mathematically precise, conceptually natural and syntax-independent manner. Surprisingly, however, game semantics of MLTT has been missing for two decades due to the difficulty in modeling type dependency in terms of games. In fact, there has been only one game semantics of dependent types by Abramsky et al. established in 2015, but it is not a complete solution either: Its interpretation of sigma-types is not by games but by a general list-construction, and it does not interpret universes at all.
In this context, I have developed a game semantics of MLTT equipped with 1-, 0-, N-, pi-, sigma- and Id-types as well as a cumulative hierarchy of universes. Notably, it models every type construction (including sigma-types and universes) solely in terms of games. I have extended it further to capture proof-normalization and (higher-order) computability of MLTT. I have also equipped it with the groupoid structure so that it refutes uniqueness of identity proofs (UIP) for the first time as game semantics, which foresees its connection with Homotopy Type Theory (HoTT).
I assume that audiences are familiar with MLTT but not game semantics. I shall rather focus on main ideas and points, leaving the details to references.
14.00–16.00, Hus 5, Sal 32
Yde Venema, Institute for Logic, Language and Computation, University of Amsterdam
Some model theory of the modal μ-calculus
Abstract: The modal μ-calculus, an extension of basic modal logic with least and greatest fixpoint operators, has its roots in computer science, where it serves to unify and provide a foundation to various specification languages for programs and reactive systems. Besides this important role in formal verification, it has become increasingly clear over the years that the formalism also has a rich and beautiful meta-theory, and deserves a place in “pure” (mathematical) logic as well as in computer science.
In the talk we will discuss some model theory of the modal μ-calculus, focussing on a number of semantic properties that are of specific interest in the setting of modal fixpoint logic.
For example, call a formula ξ continuous in a proposition letter p if the map that represents the dependency of ξ on p is Scott continuous; as we will discuss, this is linked to the question whether the least fixpoint associated with this map can reached after \omega many approximations. An equivalent characterization of Scott continuity requires that if ξ is true at a certain state then there is a finite set U such that ξ remains true at the state if we restrict the interpretation of p to the set U.
Each of the properties that we consider is, in a similar way, associated with one of the following special kinds of subset of a tree model: singletons, finite sets, finitely branching subtrees, noetherian subtrees (i.e., without infinite paths), and branches. For each of these properties we provide a corresponding syntactic fragment, in the sense that a formula ξ has the given property iff it is equivalent to a formula ξ' in the corresponding fragment.
Since this formula ξ' will always be effectively obtainable from ξ, as a corollary, for each of the properties under discussion, we prove that itis decidable in elementary time whether a given μ-calculus formula has the property or not.
Our proofs for these characterization results will be automata-theoretic in nature; we will see that the effectively defined maps on formulas are in fact induced by rather simple transformations on modal automata. Thus our results can also be seen as a contribution to the model theory of modal automata.
Finally, we will link these results with expressive completeness results. Where Janin and Walukiewicz identified the modal μ-calculus as the bisimulation invariant fragment of monadic second-order logic (MSO), I will mention similar results for weak MSO on the one hand, and for PDL and the alternation-free fragment of the modal μ-calculus on the other.
The talk is largely based on joint work with Gaelle Fontaine.
10.00–12.00
Melanija Mitrović, University of Niš
An introduction to a development of the theory of constructive semigroups with apartness
Abstract: The purpose of this lecture is an introduction to a constructive development of the theory of semigroups with apartness. The focus is on E. Bishop’s approach to constructive mathematics (BISH), [1]. The theory of constructive semigroups with apartness is a new approach to semigroup theory and not a new class of semigroups.
Content of lecture:
Part 1. Semigroups - Classical background: Our work is, of course, partly inspired by classical semigroup theory. Algebraic theory of semigroups is even within CLASS a relative new discipline, with the theory proper developing in the second half of the twentieth century. Classically, a semigroup is a set with an associative binary operation defined on it. Introductional and basic study of semigroups includes a description of special elements, special subsets, ideals, Green’s relations, homomorphisms, congruences and their relationships. This part of the talk will be mostly based on [6].
Part 2. Semigroups – Intuitionistic Setting: Constructive semigroups with apartness distinguishes from their classical ‘friends’ by two significant aspects: first, we use intuitionistic logic rather than classical, secondly, our work is based on the notion of apartness (between elements, elements and sets). In the context of semigroup with apartness we examine the basic notions of special subsets and special relations. Constructive analogues of some classical theorems like, for example, Isomorphism theorems and Cayley’s theorem, will be given too. This part of the talk will be based on material given in [3,4]. Important source of ideas, notions and notations of our work is [2]. An example of application(s) of these ideas can be found in [5].
References:
10.00–11.45
Peter LeFanu Lumsdaine
Inverse diagram models of type theory, II (joint work with Chris Kapulkin)
Abstract: Last week, I motivated and set up inverse diagram models of type theory. This week, I will generalise these to homotopical inverse diagram models, providing a much larger class of models, and some fun technical challenges.
10.00–11.45
Peter LeFanu Lumsdaine
Inverse diagram models of type theory (joint work with Chris Kapulkin)
Abstract: Homotopical inverse diagrams provide a large class of models of type theory, including:
11.00–17.00
Joint Stockholm–Göteborg type theory seminar, Lecture room EA, EDIT building, Chalmers Institute of Technology, Göteborg. (Note location!)
Talks:
10.00–11.45
Erik Palmgren
On presheaf models of type theory, part 2
Continued from part 1, October 11.
10.00–11.45
Erik Palmgren
On presheaf models of type theory
Abstract: A presheaf model may be regarded as a generalisation of a Kripke model, where the frame is allowed to be a general category instead of just a partial order. In this talk we review some basic facts on such models, especially with reference to semantic structures for dependent types. We show in particular how the notion of iterated presheaves naturally give rise to contextual categories.
10.00–11.45
Johan Lindberg
Properties of the category of local sets in Intuitionistic Ramified Type Theory
Abstract:
In [Pal17] Palmgren introduces a ramified type theory based on intuitionistic logic called IRTT, which is inspired by the modern formulation of Russell’s and Whitehead’s type theory in Principia Mathematica described in [KLN02]. IRTT contains a version of the reducibility axiom but can still be shown to be predicative by interpreting it in Martin-Löf type theory.
Palmgren also introduces a category of local sets (which are terms of powertypes) in IRTT, and expects this to form a natural notion of a predicative topos.
We establish some properties of this category and, in particular, show that it is a Π-pretopos with a natural numbers object. Extending IRTT with a principle allowing for inductive definitions (due to Palmgren) and a replacement axiom we show that the category of local sets form a ΠW-pretopos.
References:
10.00–11.45
David Ellerman University of California at Riverside, University of Ljubljana
New Foundations for Information Theory
Abstract: Partitions are categorically dual to subsets, so there is a logic of partitions dual to the usual Boolean logic of subsets. The quantitative version of the logic of subsets is logical probability theory and the quantitative version of partition logic is logical information theory which is the subject of the talk: Probability : Subsets :: Information : Partitions. Logical information theory is the foundational theory that (finally) explains what information is at the most abstract logical level. All the Shannon definitions of simple, joint, conditional, and mutual entropy can be obtained from the corresponding definitions of logical entropy by a uniform requantifying transformation. This displaces the Shannon theory from being the foundational theory to being a higher-order specialized theory for coding and communication where it has been enormously successful. The talk concludes by showing how the logical concepts extend to the quantum case to provide new foundations for quantum information theory. The background paper for the talk, “Logical Information Theory: New Foundations for Information Theory,” has come out (at least online) in The Logic Journal of the IGPL. Preprint at: www.ellerman.org.
10.00–11.45
Christian Espíndola
Infinitary generalizations of Deligne’s completeness theorem
Abstract:
Given a regular cardinal κ such that κ<κ=κ (or any regular κ if the Generalized Continuum Hypothesis holds), we study a class of toposes with enough points that we call the κ-separable toposes. These are equivalent to sheaf toposes over a site with κ-small limits that has at most κ many objects and morphisms, the (basis for the) topology being generated by at most κ many covering families, and that satisfy a further exactness property T. We prove that these toposes have enough κ-points, that is, points whose inverse image preserve all κ-small limits. This generalizes the separable toposes of Makkai and Reyes, that are a particular case when κ is countable, when property T is trivially satisfied.
This result is essentially a completeness theorem for a certain infinitary logic that we call κ-geometric, where conjunctions of less than κ formulas and existential quantification on less than κ many variables is allowed. We prove that κ-geometric theories have a κ-classifying topos having property T, the universal property being that models of the theory in a Grothendieck topos with property T correspond to κ-geometric morphisms (geometric morphisms whose inverse image preserve all κ-small limits) into that topos. Moreover, we prove that κ-separable toposes occur as the κ-classifying toposes of κ-geometric theories of at most κ many axioms in canonical form, and that every such κ-classifying topos is κ-separable.
Finally, we consider the case when κ is weakly compact and study the κ-classifying topos of a κ-coherent theory (with at most κ many axioms), that is, a theory where only disjunction of less than κ formulas are allowed, obtaining a version of Deligne’s theorem for κ-coherent toposes from which we can derive, among other things, Karp’s completeness theorem for infinitary classical logic
10.00–11.45
Jacopo Emmenegger
On the local cartesian closure of exact completions
Abstract:
Carboni and Rosolini have given a characterisation of (local) cartesian closure of exact completions which unfortunately doesn’t hold in full generality, as originally claimed.
We will discuss a sufficient condition for the local cartesian closure of an exact completion, which holds in full generality. This condition was inspired by an axiom of constructive set theory, and originally applied to a constructive version of Lawvere’s ETCS.
We will see however that it naturally arises in the homotopy-theoretic context as well. In particular, it can be used to conclude that the exact completion of the homotopy category of topological spaces is locally cartesian closed.
10.00–11.45
Håkon Robbestad Gylterud
Judgement forms and well-founded categories
Abstract:
In First Order Logic with Dependent Sorts, Makkai uses a type of well-founded categories as signatures. In this talk, we will discuss how well-founded categories can be used as signatures for judgement-forms of dependent algebraic theories and type theories. We will relate Makkai’s FOLDS-signatures to Categories with Attributes, and based on this, we propose a definition of systems of dependent rules, and give examples.
(This talk was originally scheduled for May 3.)
10.00–11.45
Peter LeFanu Lumsdaine
Computads, cell complexes, and theories, II
Abstract: This is a continuation of my talk from March 15. I look at logic in terms of the “computads”/“cell complexes” picture from last time. In particular, this will shed light on why:
10.00–11.45
Benedikt Ahrens, INRIA Nantes
Displayed Categories
Abstract: A displayed category over a category C is equivalent to “a category D and functor F : D -> C”, but instead of having a single collection of objects of D” with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as a property of displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. In this talk I will give an introduction to displayed categories and present various applications. This is joint work with Peter LeFanu Lumsdaine.
10.00–11.45
Paige North, University of Cambridge
Weak factorization systems and display map categories
Abstract: In this talk, I will describe the relationship between weak factorization systems and display map categories modeling Pi, Sigma, and/or Id types. When an ambient category C is Cauchy complete, the problem of finding the structure of a display map category modeling Sigma and Id types within C reduces to a problem of characterizing weak factorization systems on C. I will describe the categories of these objects, and using this framework I will describe the relationship between display map categories modeling Id types and those modeling Pi types.
10.00–11.45
Henrik Forssell
On a class of theories of presheaf type, II
Abstract: A geometric theory is said to be of presheaf type if it classified by a presheaf topos. We review elements of the theory of such theories and discuss some related ongoing joint work with Håkon R. Gylterud. This is the continuation of the seminar with the same title given in November 2016. We will begin with a quick recap of the material covered in that talk.
10.00–11.45
Per Martin-Löf
Assertion and request
Abstract: Think of the content of an assertion as something that is to be done: let us call it a task. Peirce’s explanation of the speech act of assertion as the assuming of responsibility then takes the form: by making an assertion, you assume the responsibility, or duty, of performing the task which constitutes the content of the assertion when requested to do so by the hearer. Thus a duty on the part of the speaker appears as a right on the part of the hearer to request the speaker to perform his duty: this is an instance of what is called the correlativity of rights and duties, a fundamental principle of deontological ethics which can be traced back to Bentham. In logic, it appears as the correlativity of assertions and requests. Since nothing but assertions appear in the usual inference rules of logic, there arises the question of what the rules are that govern the correlative requests. In the case of constructive type theory, they turn out to be the rules which bring the meaning explanations for the various forms of assertion to formal expression. Thus, in analogy with Gentzen’s dictum that the propositional operations, the connectives and the quantifiers, are defined by their introduction rules, we may say that the forms of assertion are defined by their associated request rules.
10.00–11.45
Peter LeFanu Lumsdaine
Computads, cell complexes, and theories
Abstract:
What does it mean for an object to be freely generated or presented?
We all learn one answer in our first category theory course: free objects are the values of a left adjoint functor. Life, however, is not always quite so simple; there are many kinds of “free presentation” which this does not suffice to describe. Computads and cell complexes are two more elaborate ways of freely generating/presenting an object, in settings where the specification of later generators may refer to the structure presented by earlier ones — e.g. specifying the boundary along which to glue on a new cell.
Similar issues arise with defining theories in more sophisticated logical settings. For instance, in the essentially-algebraic theory of a category, the domain of the composition operation refers to the source and target operations. Finally, the issue occurs most thornily in specifying the rules of a complex type theory.
10.00–11.45
Erik Palmgren
Intuitionistic Ramified Type Theory
Abstract: In this talk we examine the natural interpretation of a ramified type hierarchy into Martin-Löf type theory with an infinite sequence of universes. It is shown that under this interpretation some useful special cases of Russell’s reducibility axiom are valid. This is enough to make the type hierarchy usable for development of constructive mathematics. We present a ramified type theory IRTT suitable for this purpose. IRTT allows for all the basic set-theoretic constructions.
10.00–11.45
Christian Espíndola
Recovering an infinitary first-order theory from its category of models
Abstract: Makkai’s reconstruction result allows to recover a first-order theory, up to pretopos completion, by equipping the category of models with appropriate structure and considering set-valued functors preserving this structure. One of the difficulties in extending this result to the infinitary case is that the Keisler–Shelah isomorphism theorem, which asserts that elementary equivalent models have isomorphic ultrapowers, does not hold for infinitary logic. However, we will see that the theory of accessible categories can provide extra structure, under appropriate large cardinal assumptions, to recover the theory up to a notion of infinitary pretopos-completion.
10.00–11.45
Peter LeFanu Lumsdaine
A general definition of dependent type theories
Abstract:
We propose a general definition of (syntactic presentations of) type theories which yields, as instances, Martin-Löf’s various type theories (intensional, extensional, …) and their various later extensions by further type- and term-formers — inductive families, inductive-recursive types à la Dybjer/Setzer, the various higher inductive types of Homotopy Type Theory, and so on.
The novelty compared to existing approaches (logical frameworks, …) is that it yields not some embedded counterpart of a theory, whose equivalence with the original theory may be non-trivial, but literally the original type theory itself as it would typically be presented in a paper.
The need for such a framework has been sorely felt recently, since without one, theorems in the meta-theory of type theory can be stated and proved only for specific type theories (usually just small toy examples), not in the natural generality in which they are believed to hold.
It is a truism of implementation that fully precise definitions of type theories are so large and intricate as to be almost impossible to get right without extensive debugging — almost (though not quite) all presentations in the prose literature contain some errors (usually minor). To this end, we are formalising the present definition in Coq, to give confidence in its rigour and fitness-for-purpose.
10.00–11.00, Andrej Bauer, University of Ljubljana
A look at Andromeda
Abstract: I will show the current implementation of the Andromeda prover, which implements type theory with equality reflection. I will show several examples, discuss its capabilities, and future plans.
11.10–12.10, Maria Emilia Maietti, University of Padua
Martin-Löf’s type theory in support to the Minimalist Foundation
Abstract:
We argue that Martin-Löf’s type theory can be added as a third level to the two-level Minimalist Foundation (for short MF) conceived in [3] and completed in [1], in order to extract computable existential witnesses (even under hypothesis) from MF-proofs.
Indeed, thanks to results in [2] we show that the existence of a realizability model of (the intensional level of) MF advocated in [3] where to extract computable existential
witnesses from MF-proofs is not an option but a need.
[1] M.E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, 2009.
[2] M.E. Maietti. On choice rules in dependent type theory. LNCS volume of TAMC 2017
[3] M.E. Maietti and G Sambin. Toward a minimalist foundation for constructive mathematics. In L. Crosilla and P. Schuster, editor, From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, number 48 in Oxford Logic Guides, pages 91-114. Oxford University Press, 2005.
13.40–14.40 , Nicola Gambino, University of Leeds
Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures
Abstract: Working in the IZF, the assigment mapping a set X to the class of its subsets Pow(X) can be easily be shown to be part of a monad thanks to the power set axiom. But working in CZF, which does not have the power-set axiom, this assignment is only part of a “relative monad”, a notion defined by Altenkirch, Chapman and Uustalu. A similar situation arises in category theory: the assignment mapping a small category C to its category of presheaves Psh(C) is not a monad, but this time this is both because of size reasons (even working in IZF) and coherence reasons (the axioms for a relative monad do not hold strictly). In this talk, I will introduce the notion of a relative pseudo-monad, which axiomatizes the essential properties of the presheaf construction, and illustrate some of its applications, including a conceptual reconstruction of a 2-categorical model of linear logic and the differential lambda-calculus. This is joint work with Marcelo Fiore, Martin Hyland, and Glynn Winskel, presented in the preprint arXiv:1612.03678.
14.50–15.30, Henrik Forssell, Stockholm University / University of Oslo
Constructive reflection principles for regular theories
Abstract TBA.
10.00–11.45
Andrej Bauer, University of Ljubljana
Derivations as computations
Abstract:
An inference rule in type theory, or generally in a formal system, is a syntactic form which requires an interpretation. A standard reading of inference rules is that they are the closure conditions, or inductive constructors, which generate derivations. Therefore derivations are well-founded trees, freely generated by the inference rules.
I will entertain the possibility that derivations need not be freely generated by the rules. The basis for such a speculation is the observation that derivation trees represent processes for establishing judgments, but are not the processes themselves. Indeed, a mathematician’s mind most certainly does not contain derivation trees, but instead arrives at a conclusion through a mental process that can be viewed as traversal of a derivation tree. Similarly, a derivation in a proof assistant exists only implicitly in the execution trace of the program.
Once we allow inference rules to be interpreted as general operations, rather than data constructors, appealing possibilities arise. For instance, an inference rule can be read as a proof transformation, or as a computation which may have a side-effect, one of which is proof irrelevance. When these ideas are pushed into practice, they motivate the design of a proof assistant in which inference rules correspond to algebraic operations whose interpretation can be specified by the user.
[The halftime break may be extended in case audience members wish to attend Jesper Carlström’s talk “Formella metoder för järnväg”, 10:45–11:15.]
10.00–11.45
Luiz Carlos Pereira, PUC-Rio/UERJ/CNPq
Atomic Polymorphism and schematic rules: a view from proof-theory
Abstract: (joint work with Edward Hermann Haeusler, PUC-Rio) Translations have been put to many uses in logic. In the first half of last century, translations played an important role in foundational matters: the reduction of foundational questions to constructive settings. In the sixties translations became an autonomous topic: several general approaches to translations were proposed (proof-theoretical, algebraic). Another possible use of translation is related to schematic rules of inference. In 1978, Prawitz proposed an answer to the following interesting and natural questions: What’s an introduction rule for an operator φ? What’s an elimination rule for φ? Prawitz’ answer was given by means of schematic introduction and elimination rules. Prawitz also proposed a constructive version of the well-known classical truth-functional completeness: if the introduction and elimination rules for an operator φ are instances of the schematic introduction and elimination rules, then φ is intutionistically definable. Peter Schröder-Heister showed how to obtain this completeness result for higher-level schemata. These schematic introduction and elimination rules can also be used to show that logics whose operators satisfy the schematic rules and whose derivations satisfy the sub-formula principle can be translate into minimal implicational logic. Fernando Ferreira and Gilda Ferreira proposed still another use for translations: to use the Russell-Prawitz translation in order to study the proof-theory of intuitionistic propositional and first-order logic. This study is done in the atomically polymorphic system Fat. This system can be characterized as a second order propositional logic in the language {∀1, ∀2, →} such that ∀2-elimination is restricted to atomic instantiations. The aim of the present paper is to use atomic polymorphism to study the proof theory of schematic systems.
10.00–11.45
Valery Isaev, JetBrains Research / St Petersburg Academic University
Morita equivalence between homotopy type theories
Abstract: Dependent type theories have many different constructions (such as sigma, pi, inductive types, universes, and so on). We describe a general notion of dependent type theory such that each of these individual constructions gives an example of such theory. These theories are organized into a category, so we can compare them and since this category is cocomplete, we can combine individual theories to obtain theories with several constructions. Finally, we consider theories with intensional identity types (which we might call homotopy type theories). Then it is natural to consider a notion of weak equivalence between such theories which we call Morita equivalence. Often we have two theories such that some rule holds in one of them judgementally and in the other one only propositionally. Then these theories are not isomorphic, but still can be Morita equivalent.
10.00–11.45
Mateus de Oliveira Oliveira, University of Bergen
Ground Reachability and Joinability in Linear Term Rewriting Systems are Fixed Parameter Tractable with Respect to Depth
Abstract:
The ground term reachability problem consists in determining whether a given variable-free term $t_1$ can be transformed into a given variable-free term $t_2$ by the application of rules from a term rewriting system $R$. The joinability problem, on the other hand, consists in determining whether there exists a variable-free term $t$ which is reachable both from $t_1$ and from $t_2$. Both problems have proven to be of fundamental importance for several subfields of computer science. Nevertheless, these problems are undecidable even when restricted to linear term rewriting systems.
In this work, we approach reachability and joinability in linear term rewriting systems from the perspective of parameterized complexity theory, and show that these problems are fixed parameter tractable with respect to the depth of derivations. More precisely, we consider a notion of parallel rewriting, in which an unbounded number of rules can be applied simultaneously to a term as long as these rules do not interfere with each other. A term $t_1$ can reach a term $t_2$ in depth $d$ if $t_2$ can be obtained from $t_1$ by the application of $d$ parallel rewriting steps.
Our main result states that for some function $f(R,d)$, and for any linear term rewriting system $R$, one can determine in time $f(R,d)\cdot |t_1|\cdot |t_2|$ whether a ground term $t_2$ can be reached from a ground term $t_1$ in depth at most $d$ by the application of rules from $R$. Additionally, one can determine in time $f(R,d)^2 \cdot|t_1|\cdot|t_2|$ whether there exists a ground term $t$, such that $t$ can be reached from both $t_1$ and $t_2$ in depth at most $d$. Our algorithms improve exponentially on exhaustive search (which terminates in time $2^{|t_1|\cdot 2^{O(d)}} \cdot |t_2|$) and can be applied with regard to any linear term rewriting system, irrespective of whether the rewriting system in question is terminating or confluent.
10.00–11.45
Erik Palmgren
A setoid model in a flexible framework for formalized models of type theory
Abstract:
The standard frameworks for models of type theory, categories with families (cwfs), and categories with attributes (cwas), rely on a type functor into the category of sets, T : C^op → Sets. When formalizing such models in type theory the question arises how the categories of sets should be understood? We propose a flexible variant of the cwa notion suitable for such formalizations, and exemplify its use by a setoid model for dependent type theory with Π-types. The category of sets is replaced by Fr(B), the category comprised of subsetoids of a fixed setoid B, and functions between such subsetoids. The setoid B is the bounding setoid of the cwa, and thus we name the new notion a bounded cwa. In the case of the setoid model we chose B to be (V, =_V), the setoid of iterative sets, used in Aczel’s type-theoretic model of constructive set theory.
We give details of a Coq formalization of the setoid model. The formalization is made in the context of a general toolbox for formalized models of type theories, currently in development together with Peter LeFanu Lumsdaine, and also using some previous work with Olov Wilander.
10.00–11.45
Håkon Robbestad Gylterud
Categories with definitions
Abstract: Making definitions is an essential part of mathematics. However, definitions are often seen as semantically irrelevant since one can always replace a defined term with its definition. In this seminar we will explore a notion of definition which has semantic content by relating the notion of «definition» with the notion of «construction» in the context of dependent type theory. In concrete terms we will define «categories with definitions». It will be a variation (extra structure) on «categories with attributes», a well established notion of semantics of Martin-Löf type theory. Our main result will be to exhibit an adjunction between categories with attributes and categories with definitions. One distinguishing feature of these structures is that the category can remain locally finite, even though there are types with infinitely many terms – giving categories with definitions a finitist flavour.
10.00–11.45
Henrik Forssell
On a class of theories of presheaf type
Abstract: A geometric theory is said to be of presheaf type if it classified by a presheaf topos. We review elements of the theory of such theories and discuss some related ongoing joint work with Håkon R. Gylterud.
10.00–11.45
Matthew Hendtlass, Canterbury University, New Zealand
Topological models of IZF
Abstract: Topological models are a special case of Heyting-valued models—the constructive counterpart to Boolean-valued models—and include both Beth and Kripke models. The beauty of topological models is that logical principles can be translated into topological properties (though unfortunately these tend to be very unnatural) and the construction of interesting models of constructive set theory can be reduced to the construction of interesting topological spaces. In this talk we discuss topological models of intuitionistic ZF set theory. In particular we look at which standard nonconstructive principles can and cannot be separated using topological models.
10.00–11.45
Christian Espíndola
Weak completeness of infinitary intuitionistic logics without compact cardinals
Abstract: The completeness theorem for infinitary intuitionistic logics makes an appeal to large cardinals assumptions (compactness) when the theories have arbitrary cardinality. We will see how to avoid such assumptions by weakening the notion of completeness through a restriction on the cardinality of the theories.
10.00–11.45
Paul Gorbow
Algebraic Set Theory for NF and some of its variants
Abstract: NFU is a set theory allowing for atoms, axiomatized as stratified comprehension + extensionality for sets + infinity. Any model of ZF that admits a non-trivial automorphism, may be turned into a model of NFU, by a simple reinterpretation of membership. NF is NFU + everything is a set. INF(U) is intuitionistic NF(U). In this presentation we give theories in the language of categories equiconsistent to each of (I)NF(U). Just as the theory of topoi generalizes set theory, the theory of categories of classes generalizes class theory. This is essentially a first order theory in the language of categories augmented with a predicate that distinguishes between small and large objects and morphisms. The restriction of a category of classes to its small objects and morphisms, is a topos; and conversely, any topos embeds as the small objects and morphisms in a category of classes. Categories of classes facilitate direct interpretation of traditional set theory. For example, Awodey et al. (2014), used them to interpret Basic Intuitionistic Set Theory (BIST). We focus on presenting the theory HC + PT in the language of categories augmented with a predicate distinguishing between homogeneous and non-homogeneous morphisms, and we show that it is equiconsistent to INFU. The subcategory of homogeneous morphisms stands in the analogous relation to INFU as a topos stands to BIST. (Moreover, it has a natural subcategory of “Cantorian” objects, which is a topos.) The argument is easily modified for (I)NF(U). As a corollary, we obtain a new proof of Con(NF) iff Con(NFU + |V| = |P(V)|).
No seminar.
10.00–11.45
David Fernández-Duque, Centre International de Mathématiques et d’Informatique de Toulouse
The (poly)topologies of provability logic
Abstract:
The Gödel-Löb logic GL is a modal logic which is sound and complete for its arithmetical interpretation, where the modal [] represents Gödel’s provability predicate. It also enjoys both relational and topological semantics, the latter based on Cantor’s scattered spaces. There are various completeness results for this interpretation, due to Esakia, Abashidze and Blass.
Meanwhile, Japaridze’s polymodal logic GLP is an extension of GL which has one modality [n] for each natural number. These operators also enjoy a natural proof-theoretic interpretation using a notion of n-provability, but in contrast to GL, GLP is incomplete for its relational semantics. Fortunately, it is complete for its topological interpretation, using polytopological spaces with an increasing chain of scattered topologies, as was shown by Beklemishev and Gabelaia. The proof of this is non-constructive and required novel techniques in the study of scattered spaces. Moreover, as the speaker has shown, this result also holds for Beklemishev’s transfinite extension of GLP.
In this presentation, we will introduce the logics GL and GLP along with their intended proof-theoretic interpretation. We will discuss their relational and topological semantics, and sketch the main ideas behind the completeness proofs for the latter.
10.00–11.45
Benno van den Berg, Institute for Logic, Language, and Computation, University of Amsterdam
Arithmetical conservation results and Goodman’s Theorem
Abstract:
A well–known result by Goodman [1] states that Heyting arithmetic in all finites types together with the axiom of choice for all types is conservative over Heyting arithmetic. Goodman’s original proof was quite complicated and many people have since tried to give more perspicuous proofs of his theorem, including Goodman himself, Beeson, Renardel de Lavalette, Coquand and possibly others. In this talk I will present my preferred proof, developed together with Lotte van Slooten, which combines ideas from all these authors and adds some new ones.
[1] N.J. Goodman, The theory of Gödel functionals, Journal of Symbolic Logic 41 (3), 1976, pp. 574–582
Hus 5, Rum 14 (note place!)
Christian Espíndola
PhD Thesis Defense
Hus 5, Rum 16
Marek Zawadowksi, University of Warsaw
Scope-taking with continuations: scope ambiguities, monads and strengths
Abstract: In this talk, we discuss three semantically distinct scope assignment strategies for simple multi-quantifier sentences: traditional movement strategy (May, 1977), polyadic approach (May, 1985), and continuation-based approach (Barker, 2002). Both the polyadic approach and the continuation-based strategy make heavy use of the computational machinery connected to the continuation monad - strength and derived operations. The continuation-based strategy advocates itself as a compelling alternative to the traditional movement strategy and polyadic approach for providing a uniform non-movement (in situ) analysis of quantifiers. However, it cannot be straightforwardly extended to account for sentences involving 3 quantifier phrases - it only provides four out of six readings accounted for by the two other strategies. We shall show how one can augment the continuation-based strategy (as in Barker, 2002) to obtain the two missing readings.
Hus 5, Rum 16
Justyna Grudzinska, University of Warsaw
Scope-taking with dependent types: relational nouns, inverse linking and long-distance indefinites
Abstract: In this talk, we discuss two puzzling scope facts occurring in complex syntactic environments: inverse linking and long-distance indefinite readings. First, we develop a new account of the so-called relational nouns (e.g. representative, solution) from the perspective of our semantics combining generalized quantifiers with dependent types [1]. Whereas in the Montagovian setting relational nouns are interpreted as two-place relations (expressions of type <e,<e,t>>), our framework allows us to interpret them as dependent types. Then, we use our dependent type account of relational nouns to tackle the two puzzling scope phenomena in question. The solution to the puzzle of long-distance indefinites extends our earlier proposal in [2] and [3].
10.00–11.45
Peter LeFanu Lumsdaine
The 2-category of comprehension categories, II
Abstract: Continuing from last week’s seminar, I will use the 2-categorical setting to define a general notion of rules and logical structure on comprehension categories — general enough to cover most (?all) standard logical constructors of dependent type theory, but (hopefully) specialised enough to still admit various standard constructions and meta-theorems.
10.00–11.45
Peter LeFanu Lumsdaine
The 2-category of comprehension categories
Abstract:
Comprehension categories, introduced by Bart Jacobs, are a generalisation of categories with attributes, contextual categories, and so on — so, yet another categorical structure for the semantics of type theory.
Their unique selling point is that they are flexible and general enough to capture both the strict substitutivity properties enjoyed by syntax, and the weaker pullback-stability properties typically found in models. They thus form a good setting for defining and comparing such stability properties.
I will discuss how a 2-categorical viewpoint can be fruitful in the study of comprehension categories.
10.00–11.45
Jacopo Emmenegger
Exact completion and constructive theories of sets
Abstract: In this talk I will present Palmgren’s constructive modification (CETCS) of Lawvere’s Elementary Theory of the Category of Sets (ETCS), explain how the theory of exact completions tells us that any category satisfing such axioms is a free exact category, and isolate the weaker properties that a projective cover of an exact category C has to satisfy in order for C to be a CETCS category. In particular, Carboni and Rosolini already have a characterisation of local closure in terms of weak closure of the maximal projective cover, but I will explain how some model-theoretic observations strongly suggest that it cannot be applied to our case. Therefore I will introduce an alternative characterisation of closure for free exact categories, which applies to any projective cover. This is joint work with Erik Palmgren.
10.00–11.45
Peter LeFanu Lumsdaine
An accessible treatment of transfinite constructions
Abstract:
Transfinite constructions for building free objects, and more generally objects specified by presentations (generators and relations, etc), are ubiquitous in mathematics. Max Kelly’s 1980 paper “A unified treatment of transfinite constructions” provides very powerful and general categorical results, yielding many such situations as instances of a single general construction. However, due to its great generality, the paper is a little forbidding to the reader looking to unwind the details of any particular instance. (It has been suggested that it is cited more often than it is read.)
I will describe concretely how the construction works for a moderately general range of common use-cases: most importantly, free monads on (pointed) endofunctors, and more generally, certain presented monads. The presentation I will give, in terms of “T-graphs”, is based on that of Koubek and Reiterman 1978 “Categorical constructions of free algebras…”
10.00–11.45
Steve Awodey, Carnegie Mellon University, Pittsburgh
Homotopy type theory: A cubical algebraic weak factorization system.
Abstract: Fourth and final lecture in the series. We prove that the category of cartesian cubical sets carries an algebraic weak factorization system in which every fibration admits the canonical pathobject factorization of the diagonal map. As a consequence, the cubical semantics for Martin-Löf type theory developed in the previous lectures soundly model all the rules for identity types.
10.00–11.45
Hannes Diener, University of Canterbury, NZ
Completeness is overrated
Abstract: It is a common theme in constructive mathematics that adding completeness to the assumptions often allows us to prove otherwise constructively unprovable statements. In this talk we show that we actually only need a very weak version of completeness. We also show that there is an enormous amount of spaces that aren’t complete, but satisfy the weakened version of completeness, thus generalising many theorems of constructive analysis.
10.00–11.45
Maarten McKubre-Jordens, University of Canterbury, NZ
Material implications over minimal logic
Abstract: The “atrocities” of material implication have motivated the development of many non-classical logics over the years. In this talk, we outline some of these paradoxes and classify them over minimal logic. We provide some proofs of equivalence and semantic models separating the paradoxes where appropriate. A number of equivalent groups arise, all of which collapse with unrestricted use of double negation elimination. Principles weaker than ex falso quodlibet turn out to be distinguishable, even with a logic so little “mutilated” as minimal logic. This can be interpreted in at least two ways: even minor changes to the logic underpinning mathematical reasoning allow many more distinctions than the classical understanding; and supporting motivation for adopting minimal logic as the ambient logic for mathematical reasoning in the possible presence of inconsistency.
10.00–11.45
Erik Palmgren
Categories with families and FOLDS: hyperdoctrines and logic over dependent sorts.
Abstract: This is a sequel to the seminar of February 24. We consider various formulations of logic over dependent sorts, with semantics in hyperdoctrines relative to categories with families.
10.00–11.45
Peter LeFanu Lumsdaine
Comparing algebraic structures for semantics of type theory
Abstract:
In 1986, John Cartmell introduced contextual categories as an algebraic tool for working with models of type theories. In the thirty years since, many variations on these have been introduced: categories with families, categories with attributes, type-categories, comprehension categories, C-systems, … To add to the fun, some of these names have been given slightly different definitions by different authors.
They are all closely related, and some but not all are precisely equivalent. I will survey the relationships between them, and their implications for modelling type theory. This is in part a report on work in progress with Benedikt Ahrens and Vladimir Voevodsky, in which we formalise some of the comparisons in question.
10.00–11.45
Per Martin-Löf
Dependent Contexts and Substitutions
14.30–16.15, in room 22, building 5. (Note nonstandard location!)
Martín Escardó
Mathematical degrees of existence in type theory
Abstract:
Constructive mathematics is often equated with computation. But
perhaps a better view (compatible with computation) is that
constructive mathematics is about information: information we give,
and information is offered to us. In classical mathematics what
matters about a theorem is its truth, whereas in constructive
mathematics what matters is how much information its formulation and
proof give.
A particular case of existence is disjunction. For example, in
classical mathematics, Goldbach’s Conjecture holds or it doesn’t (by
the excluded-middle postulate). But (both classical and constructive)
mathematicians still want to know which one is the case. An answer to
the second question gives more information. In constructive systems
such as type theory, it is possible to express mathematically the
difference between the information content of the first and second
situations.
In this talk I want analyse, mathematically (rather than
meta-mathematically or philosophically), the notion of existence in
terms of information content. I will show, with definitions, theorems,
proofs and examples, that there are many (constructive) degrees of
existence, distinguished by the amount of information they give/get.
I will perform this mathematical analysis in Martin-Loef type theory
and some univalent extensions. In particular, I will discuss Brouwer’s
continuity axioms, some of which become false, when rendered in MLTT,
if too much existential information is required.
No seminar this week due to the 27th Nordic Congress of Mathematicians, March 16–20, Frescati.
10.00–11.45
Håkon Robbestad Gylterud
Strong collection, subset collection and the identity type
Abstract: Strong collection and subset collection are two axioms of constructive set theory. They are distinct from other set theoretical axioms in that they claim existence of certain sets, but do not characterise these sets precisely. Their constructive justification is closely tied to Aczel’s model of constructive set theory in type theory, and the notion of operation versus the notion of function. I will in this talk discuss these axioms in the context of a model where the interpretation of equality is the identity type. As it turns out, it is instructive to first consider the equivalents of these axioms for multisets.
10.00–11.45
Erik Palmgren
Categories with Families and FOLDS: functorial semantics vs standard semantics
Abstract: Every dependent first-order signature Sigma generates a free category with families F(Sigma). A model C of the Sigma-signature is a cwf morphism M from F(Sigma) to C. Such a morphism is uniquely determined by its values on the signature. We show that such morphisms can constructed by incrementally by induction on the signature. This shows that this functorial notion of model extends the usual non-dependent version of model of first-order signature.
10.00–11.45
Roussanka Loukanova
Gamma-Reduction in Type Theory of Acyclic Recursion
Abstract: I will introduce Moschovakis Type Theory of Acyclic Recursion (TTAR) by extending its reduction system. The extended TTAR has potentials for more efficient computational semantics of formal and natural languages. At first, I will present the original reduction calculus of TTAR, which reduces TTAR-terms to their canonical forms. The canonical forms of the terms determine the algorithms that compute their semantic denotations, and, in addition, the relation of algorithmically referential synonymy between TTAR-terms. The lambda-rule, which is the most important rule of the reduction calculus of TTAR, strictly preserves the algorithmic structure of the reduced terms. However, in its original, general formulation, the lambda-rule may result in superfluous lambda abstractions in some parts of the terms. In the second part of the talk, I introduce the gamma-rule, which extends the reduction calculus of TTAR and its referential synonymy to gamma-reduction calculus and gamma-synonymy, respectively. The gamma-rule is useful for simplifying terms. It reduces superfluous lambda-abstraction and corresponding functional applications in the terms, while retaining the major algorithmic structure of the terms.
10.00–11.45
Johan van Benthem, Universiteit van Amsterdam
Dynamic-Epistemic Logic, Information and Tracking
Abstract: We review basics of dynamic-epistemic logics for agent attitudes of knowledge and belief, plus stepwise effects of events leading to information and belief change. Then, we introduce more fine-grained neighborhood models for ‘evidence’, and their richer set of attitudes and dynamic events. Next, we study how dynamics at one ‘zoom level’ can, or cannot, track the dynamics at another level, using natural inter-level maps. Finally, we discuss a total logical picture of how information functions.
References:
J. van Benthem, 2011, Logical Dynamics of Information and Interaction, Cambridge University Press, Cambridge UK.
—, 2015, ‘Tracking Information’, in K. Bimbó, ed., Mike Dunn on Logic and Information, Outstanding Contributions to Logic, Springer, Dordrecht.
10.00–11.45
Per Martin-Löf
The two interpretations of natural deduction: how do they fit together?
10.00–11.45
Michael Makkai, McGill
FOLDS equivalences as the basis of a general theory of identity for concepts in higher dimensional categories, part 2
10.00–11.45
Michael Makkai, McGill
FOLDS equivalences as the basis of a general theory of identity for concepts in higher dimensional categories, part 1.
Abstract (for part 1 and 2): 1. The theory of abstract sets is based on a formal language that is given within FOLDS, first-order logic with dependent sorts. Abstract set theory was introduced in an informal manner by F. W. Lawvere in Section 2 of his 1976 paper “Variable quantities and variable structures in topoi”. Lawvere used his informal, but very informative description of abstract set theory for the purposes of topos theory. In 2003, and then in a more detailed manner in 2013, I introduced the formalization I will talk about here. It is more directly set-theoretical than topos theory, which is based on the language of categories. The structuralist imperative, stated by Bourbaki as an explicit requirement on any concept of structure, a special case of which is that “an abstract set has no external properties save its cardinality” (Lawvere), appears, necessarily in the absence of a formal language, as a desideratum in Lawvere’s exposition. The main result of my work is that in the new formalization, the structuralist imperative becomes a provable general fact, in the form that any concept formulated in the dependent-typed language of abstract sets is invariant under isomorphism.
I will use the opportunity of abstract sets to introduce, albeit only in an informal way, the general syntax of FOLDS.
2. I introduced FOLDS in 1995 in the monograph “First Order Logic with Dependent Sorts with Applications to Category Theory” (available on my web-site both in its originally typed and also in a TEXed version). In the paper “Towards a Categorical Foundation of Mathematics”, published in 1998, but written at the same time as the monograph in 1995, I gave a descriptive outline of the theory. The syntax is explained both symbolic-logically, and by using tools of categorical logic. The main reason why I came out with FOLDS is that I found that there is a notion generalizing isomorphism — called FOLDS equivalence — for structures for a FOLDS language such that:1) many (all?) notions of equivalence used in higher- dimensional categories coincide with appropriate instances of the FOLDS equivalence, and 2) first-order properties of structures in general are invariant under FOLDS equivalence if and only if they are equivalently formulatable in the FOLDS syntax. My main application of FOLDS is a statement of the universe of the so-called multitopic categories; see The Multitopic Category of All Multitopic Categories on my web-site, in both the 1999 and the corrected 2004 versions. In the talk, I will necessarily be rather informal about the subject, with suggestive examples rather than precise general definitions.
10.00–11.45
Dag Westerståhl
The meaning of ▢ and other logical constants
Abstract: We study the extent to which logical consequence relations in a language L determine the meaning of the logical constants of L. For example: Do the laws of classical logical consequence in first-order logic fix the meaning of ∀? Carnap asked this question in 1943 about the connectives in classical propositional logic (and implicitly answered it). In [1], we extended this result to first-order logic, and to the framework of possible worlds semantics. In this talk, which is about work in progress, I consider the same question for some intensional logics. First, there are two simple observations on the interpretation of the connectives in intuitionistic propositional logic, in the setting of Kripke semantics. Then I focus on modal logic. Roughly, what range of interpretations of ▢ do various (normal) modal logics allow? Some results and some open issues will be presented. This is joint work with Denis Bonnay.
[1] D. Bonnay and D. Westerståhl, ‘Compositionality solves Carnap’s Problem’, Erkenntnis 80 (4), 2015 (online first).
10.00–11.45
Andrew Swan, Leeds
Identity types in Algebraic Model Structures
Abstract: The original Bezem-Coquand-Huber cubical set model promised to give a constructive model of homotopy type theory. However, in its original form there was a notable shortcoming: one of the definitional equalities usually included in type theory, the J computation rule was absent. One way to fix this is to use an alternative definition of identity type in which we keep track more carefully of degenerate paths. The new identity type has a nice presentation in the setting of algebraic model structures. To model identity types what we need is very good path objects: a factorisation of each diagonal as a trivial cofibration followed by a fibration. I’ll show a general way to create very good path objects from path objects in the weaker sense of factorisations of diagonals as weak equivalence followed by fibration, and that under certain reasonable conditions on an ams this can be carried out "stably and functorially" allowing us to satisfy the Garner-van den Berg notion of "stable functorial choice of diagonal factorisation." I’ll use these ideas to show that in particular cubical sets with Kan fibrations satisfy Garner and van den Berg’s notion of homotopy theoretic model of identity types. In this way we get a constructive proof that cubical sets model intensional type theory including all definitional equalities, dealing with coherence issues directly without using universes or local universes and retaining any propositions from the original BCH model, including univalence.
10.00–11.45
Eric Finster, Eric Finster, EPFL Lausanne
Towards an Opetopic Type Theory
Abstract: The realization that dependent type theory has a higher categorical interpretation where types are coherent higher groupoids has been a major development in the field. However, while internally types exhibit coherent structure provided by their identity types, type theory itself still lacks any mechanism for describing more general coherent objects. In particular, it has no means of describing higher equivalence relations (i.e. internal higher groupoid objects) or coherent diagrams of types (functors into the universe). Much work has focused on the search for reasonable internal notion of simplicial types to remedy this problem, but to date no simple solution has been found. In this talk, motivated by recent progress in formalizing the Baez-Dolan opetopic definition of higher categories in type theory, I will present an alternative approach to coherence based on opetopes. The theory of opetopes is based on the theory of polynomial functors, also known as as W-types or containers in the type theory literature, and thus fits naturally with concepts already familiar from logic and computer science. I will sketch a type theory extended with syntax for manipulating opetopic expressions a explain how this leads to a quite general logical theory of coherence.
10.00–11.45
Peter LeFanu Lumsdaine
Equivalences of (models of) type theories, continued
Abstract: Continuing from last week’s seminar, I will go into the details of the logical structure in the models in spans and span-equivalences. I will also lay out some more abstract nonsense about categories of contextual categories, and use this to give applications of the span-equivalences model to the "homotopy theory of homotopy type theory".
10.00–11.45
Peter LeFanu Lumsdaine
Equivalences of (models of) type theories
Abstract: (joint work with Chris Kapulkin) I will present a new model of type theory in "span-equivalences" over a given model, based on the model in spans or basic pairs (as given by Simone Tonelli and by Mike Shulman). This "span-equivalences" model provides a useful technical tool for reasoning about equivalence between models of type theories. I will describe (at least) two applications: firstly, that once the interpretation of contexts, types, and terms has been fixed, the interpretation of the rest of type theory is determined up to equivalence; and secondly, a presentation of the "homotopy theory of models of type theory". This is work in progress, and suggestions of further applications are very welcome!
10.00 - 11.45 in room 22, building 5, Kräftriket, Stockholm. (Note unusual location!)
Valentin Goranko
Logics for visual-epistemic reasoning in multi-agent systems
Abstract. In this talk I will present a logical framework for multi-agent visual-epistemic reasoning, where each agent receives visual information from the environment via mobile camera with a given angle of vision in the plane. The agents can thus observe their surroundings and each other and can reason about each other’s observation abilities and knowledge derived from these observations. I will introduce suitable logical languages for formalising such reasoning, involving atomic formulae stating what agents can see, multi-agent epistemic operators, as well as dynamic operators reflecting the ability of agents (or, their cameras) to move and turn around. I will then introduce several different types of models for these languages and will discuss their expressiveness and some essential validities. Lastly, I will discuss some basic model-theoretic problems arising in this framework that open up new directions of study, relating logic, geometry and graph theory.
This talk is partly based on a recent joint work with Olivier Gasquet (Univ. Paul Sabatier, IRIT, Toulouse) and Francois Schwarzentruber (ENS Rennes).
10.00 - 11.45
Raazesh Sainudiin, University of Canterbury, Christchurch, N.Z.
An Interval Tree Arithmetic for Computationally Amenable Operations with Maps in Some Metric Spaces
Abstract: I will spend the first part of the talk on an introduction to interval analysis (for general maths audience). In the second part of the talk I will introduce an arithmetic with planar binary trees that are used to represent maps and show how this is used to solve some concrete real-world problems, including nonparametric density estimation, dynamic air-traffic representation, tighter range enclosures of interval-valued functions that can be expressed via finitely many real arithmetic operations, and simulation from challenging densities in up to 10 dimensions.
References:
http://tinyurl.com/oxrgse4
http://tinyurl.com/pakpny9
http://dx.doi.org/10.1145/2414416.2414422
http://arc.aiaa.org/doi/abs/10.2514/1.I010015
10.00–11.45
Erik Palmgren
Progress report on formalizing categories with attributes in type theory, part 2
Abstract: This talk is a follow up of the talks by Peter Lumsdaine and myself respectively, last term on this subject. A complete formalization in Coq of bounded categories with attributes and structures for type theory with one universe, has since then been achieved. We indicate how a setoid model of type theory is constructed via the use of a formalized model of CZF.
10.00–11.45
Per Martin-Löf
Spreads, repetitive structures, and functional causal models
Makoto Fujiwara, JAIST
Constructive provability versus uniform provability in classical computable mathematics
Abstract: So-called elementary analysis EL is two-sorted intuitionistic arithmetic, which serves as system to formalize constructive mathematics. In this talk, we show that for any Pi^1_2 formula T of some syntactical form, T is provable in EL if and only of T is uniformly provable in classical variant RCA of EL. It is remarkable that all of our proofs are constructive, namely, they are just explicit syntactic translations. Since a large number of existence theorems are formalized as Pi^1_2 formula T of the form, under the agreement that constructive provability is identical with provability in EL, it suggests the constructive equivalence (from a meta-perspective) between constructive provability and classical uniform provability in RCA for practical existence theorems.
15.00–16.00, in room 306, building 6, Kräftriket,
Ulrik Buchholtz, Carnegie-Mellon University
Weak dependent type theories
Abstract: I’ll discuss ongoing work on formulating proof-theoretically weak dependent type theories (of strength polytime and primitive recursive) that permit some higher type and large eliminations. Motivations include constructive reverse mathematics and eventually also a weak homotopy type theory.
10.00–11.45
Erik Palmgren
Progress report on formalizing categories with attributes in type theory
Abstract: This talk is a complement to the talk by Peter LeFanu Lumsdaine earlier this term on a joint project with him and Håkon Gylterud.
10.00–11.45
Chris Kapulkin, University of Western Ontario
Type theory and locally cartesian closed quasicategories
Abstract: Let T be a dependent type theory admitting the rules for Pi-, Sigma-, and Id- types, and let C(T) be its syntactic category, that is, the category whose objects are contexts and whose morphisms are (sequences of) terms. This category is naturally equipped with a class of syntactically defined weak equivalences and as such presents some quasicategory. It is then natural to ask what can we say about this quasicategory. After explaining the necessary background, I will show a proof that the quasicategories arising this way are locally cartesian closed. This answers the question posed by Andre Joyal in his talk at the Oberwolfach mini-workshop on HoTT in 2011.
10.00–11.45
Christian Espíndola
Completeness of infinitary intuitionistic logics
Abstract: In this talk I will present the second half of my thesis, which relies on classical assumptions and is meant to be a counterpart for the constructive content of the first half. We will define formal systems for infinitary intuitionistic logics and prove completeness theorems in terms of a natural infinitary Kripke semantics, both in the propositional case and the first-order case. The metatheory will be ZFC plus the existence of weakly compact cardinals, a large cardinal assumption that will also be proved to be necessary for the completeness results to hold. We will also review some applications and consequences of these results.
10.00–11.45
Peter LeFanu Lumsdaine
Martin Hofmann’s conservativity theorems
Abstract: Two notable conservativity results in dependent type theory are due to Martin Hofmann: the conservativity of the logical framework presentation of a type theory, and the conservativity of extensional type theory over intensional type theory with extensionality axioms.
I will discuss these two theorems, and the general status of conservativity results in dependent type theory.
This will be an entirely expository talk.
10.00–11.45
Steve Awodey, Carnegie Mellon University
Cubical Homotopy Type Theory
Abstract: In this work-in-progress talk, I will analyse the cubical model of homotopy type theory of Coquand et al. in functorial terms, making a few modifications along the way. The basic category of cubical sets used is presheaves on the free cartesian category on a bipointed object, i.e. the Lawvere theory of bipointed objects. The presheaf category is the classifying topos for strictly bipointed objects.
The Kan extension property familiar from algebraic topology is shown to be exactly what is required to model the Identity-elimination rule of Martin-Löf, and the closure of Kan objects under function spaces is ensured constructively by Coquand’s uniformity condition, re-analysed as the existence of a certain natural transformation making natural choices of Kan fillers. A universe of Kan objects is given in the style of the recent “natural models” construction, based on ideas of Lumsdaine-Warren and Voevodsky.
10.00–11.45
Peter Aczel, Manchester University
On the Consistency Problem for Quine’s New Foundations, NF
Abstract: In 1937 Quine introduced an interesting, rather unusual, set theory called New Foundations - NF for short. Since then the consistency of NF has been an open problem. And the problem remains open today. But there has been considerable progress in our understanding of the problem. In particular NF was shown, by Specker in 1962, to be equiconsistent with a certain theory, TST^+ of simple types. Moreover Randall Holmes, who has been a long-term investigator of the problem, claims to have solved the problem by showing that TST^+ is indeed consistent. But the working manuscripts available on his web page that describe his possible proofs are not easy to understand - at least not by me.
In my talk I will introduce TST^+ and its possible models and discuss some of the interesting ideas, that I have understood, that Holmes uses in one of his possible proofs.
10.00–11.45
Maarten McKubre-Jordens, University of Canterbury, NZ
Mathematics in Contradiction
Abstract: Advances in paraconsistent logics have begun attracting the attention of the mathematics community. Motivations for the development of these logics are wide-ranging: expressiveness of language; a more principled approach to implication; robustness of formal theories in the face of (local) contradiction; founding naive intuitions; and more. In this accessible survey talk, we outline what paraconsistency is, why one might use it to do mathematics, discuss some of the triumphs of and challenges to doing mathematics paraconsistently, and present some recent results in both foundations and applications. Applying such logics within mathematics gives insight into the nature of proof, teases apart some subtleties that are not often recognized, and gives new responses to old problems. It will turn out that despite the relative weakness of these logics, long chains of mathematical reasoning can be carried out. Moreover, in handling contradictions more carefully, paraconsistent proofs often bring out subtle differences between proofs that are often overlooked - not all proofs are created equal, even when truth (or falsity!) is preserved.
10.00–11.45
Henrik Forssell
Constructive completeness (continued)
Abstract: We give an analysis of some long-established constructive completeness results in terms of categorical logic and pre-sheaf and sheaf semantics, and add some new results in this area which flow from the analysis. Several completeness theorems are derived without the assumption that equality of non-logical symbols in the language can be decided. This is joint work with Christian Espíndola. The talk summarizes and continues some of the previous presentations by Espíndola and Forssell on the subject.
10.00–11.45
Peter LeFanu Lumsdaine
Progress report: formalising semantics of type theory in type theory.
10.00–11.45
Per Martin-Löf
Invariance of causal space-time (cont.).
10.00–11.45
Per Martin-Löf
Invariance of causal space-time
10.00–11.45
Benno van den Berg, ILLC, Amsterdam
Recent results around a nonstandard functional interpretation
Abstract: In recent work with Eyvind Briseid and Pavol Safarik we defined functional interpretations for systems for nonstandard arithmetic. We used these interpretations to prove conservation and term extraction results. In the talk I will explain the nonstandard functional interpretation could have been found without aiming for a proof-theoretic analysis of nonstandard systems, but rather by modifying certain ideas for refined term extraction. I will also discuss recent developments.
10.00–11.45
Douglas S. Bridges, University of Canterbury, Christchurch, New Zealand
Morse Set Theory as a Foundation for Constructive Mathematics
Abstract: In the northern autumn of 1972, I came across A.P. Morse’s little book ‘A Theory of Sets’, and became absorbed by the idea of carrying through a constructive development of set theory (CMST) along the same lines, in which everything was expressed in a kind of pseudocode governed by strict rules of language and notation. Such a development would seem to be particularly suitable for proof-checking and for the extraction of programs from proofs. Chapter 1 of my D.Phil. thesis (Oxford, 1974) contained the fruits of my labours to that stage. After that, despite a brief foray into CMST for a conference paper in 1986, my plan to develop the set theory in greater depth was shelved until taken up again late last year.
In this talk I sketch some of the salient features of this updated development of CMST, paying particular attention to where it deviates from Morse’s classical theory and to those results of the latter that are essentially nonconstructive
10.00–11.45
Christian Espíndola
Beth models for intuitionistic logic
Abstract: The semantics of possible worlds for intuitionistic logic gives rise to Kripke models and its variant, Beth models. Although both semantics can be shown to be complete, we will see that the later has advantages over the former in the sense that with a weaker metatheory, they describe a wider variety of categorical models. In particular, we will discuss how to build, for every model in a Grothendieck topos, an elementarily equivalent Beth model, as well as the constructive aspects and applications of this.
10.00–11.45
Erkki Luuk
A type-theoretical approach to Universal Grammar
Abstract: The idea of Universal Grammar as the hypothetical linguistic structure shared by all human languages harkens back at least to the 13th century. The best known modern elaborations of the idea are due to Chomsky (e.g. 1970, 1981, 1995). Following a devastating critique from theoretical (e.g. Jackendoff 2002), typological (e.g. Evans & Levinson 2009) and field (e.g. Everett 2005) linguistics, these elaborations, the idea of Universal Grammar itself and the more general idea of language universals stand untenable and are largely abandoned. The talk will show how to tackle the hypothetical structure of Universal Grammar using dependent type theory in a framework very different from the Chomskyan ones.
10.00–11.45
Peter LeFanu Lumsdaine
The coherence problem for dependent type theory
Abstract: Coherence constructions are a vexing technical hurdle which most models of dependent type theory, especially homotopical ones, have to tackle in some way. I will explain what the basic problem of coherence is, and survey the main known approaches to overcoming it, including the constructions of Hofmann,Voevodsky/Hofmann - Streicher, Lumsdaine - Warren, and Curien - Garner - Hofmann.
10.00–11.45
Antti Kuusisto, Stockholm University
Uniform one-dimensional fragment of first-order logic
Abstract: In this talk we first briefly survey recent research on complexity and expressivity of weak fragments of first-order logic. Such fragments include, e.g., guarded fragments and two-variable systems. We then discuss the recently introduced uniform one-dimensional fragment (UF1), which generalizes the standard two-variable fragment in a way that leads to the possibility of defining non-trivial properties of relations of arbitrary arities. The increased expressivity does not lead to an increase in complexity: we show that UF1 is NEXPTIME-complete. The work presented is joint work with Emanuel Kieronski and Lauri Hella.
10.00–11.45
Peter Dybjer, Chalmers/Gothenburg University
Game semantics and normalization by evaluation
Abstract: We show that Hyland and Ong’s game semantics for PCF can be presented using normalization by evaluation (nbe). We use the bijective correspondence between innocent well-bracketed strategies and PCF Böhm trees, and show how operations on PCF Böhm trees, such as composition, can be computed lazily and simply by nbe. The usual equations characteristic of games follow from the nbe construction without reference to the game-theoretic machinery. As an illustration, we give a Haskell program computing the application of innocent strategies.
This is joint work with Pierre Clairambault, CNRS and ENS Lyon.
10.00–11.45
Valentin Goranko, Stockholm University
On the theories of almost sure validities in the finite in some fragments of monadic second-order logic
Abstract: This work stems from the well-known 0-1 law for the asymptotic probabilities of first-order definable properties of finite graphs (in general, relational structures). Fagin’s proof of this result is based on a transfer between almost sure properties in finite graphs and true properties of the countable random graph (aka, Rado graph). Both the transfer theorem and the 0-1 law hold in some non-trivial extensions of first-order logic (e.g., with fixed point operators) but fail in others, notably in most natural fragments of monadic second-order (MSO). The main problem of this study is to characterise, axiomatically or model-theoretically, the set of almost surely valid in the finite formulae of MSO, i.e. those with asymptotic probability 1. The set of almost sure validities in the finite of any given logical language (where truth on finite structures is well-defined) is a well-defined logical theory, containing all logical validities of that language and closed under all sound finitary rules of inference. Beyond that, little is known about these theories in cases where the transfer theorem fails. The talk will begin with a brief introduction to asymptotic probabilities and almost surely true properties of finite graphs, the 0-1 laws for first-order logic and in some extensions of it, and their relationship with the respective logical theories of infinite random graphs. Then I will focus on the almost sure theories in modal logic and in the Sigma^1_1 and Pi^1_1 fragments of MSO on binary relational structures, aiming at obtaining explicit logical characterisations of these theories. I will present such partial characterisations in terms of characteristic formulae stating almost sure existence ( Sigma^1_1) or non-existence (for Pi^1_1) of bounded morphisms to special target finite graphs. Identifying explicitly the set of target finite graphs that generate almost surely valid characteristic formulae seems a quite challenging problem, to which we so far only provide some partial answers and conjectures.
Extra type theory seminar
Ali Assaf, INRIA and École Polytechnique, Paris
Embedding logics in the lambda-Pi calculus modulo rewriting
Abstract: The lambda-Pi calculus modulo is an extension of the lambda-Pi calculus with rewrite rules. Using the Curry-Howard correspondence, it can be used as a logical framework to define logics and express proofs in those logics in a way that preserves the reduction semantics. I will show how we embed various theories such as the calculus of constructions and simple type theory in the lambda-Pi calculus modulo rewriting and consider the soundness and completeness of these embeddings.
Michael Rathjen, Leeds
Is Cantor’s continuum problem still open?
Abstract: The continuum hypothesis, CH, asserts that an infinite set of reals is either countable or of the same size as the entire continuum (so nothing exists in between). Cantor couldn’t determine the truth or falsity of CH. The quest for its status became enshrined in Hilbert’s famous 1900 list, earning it a first place. Hilbert announced a proof of CH in his 1925 talk "On the Infinite" which arguably inspired Gödel to find a model of set theory that validates CH. With the work of Cohen in the 1960s, many people were convinced that CH was now a settled problem as all essential facts about it were deeply understood. This situation, however, did not convince everybody (e.g. Gödel). The last 20 years or so have seen a resurgence of the problem in modern set theory, in particular in the work of Woodin. In the first part of the talk, I plan to survey the most important known facts about CH. This will be followed by relating some of the modern attempts at finding new axioms to settle CH. Their justifications are partly based on technical results but also tend to be highly speculative and often come enmeshed with essentially philosophical arguments. Finally I shall consider a specific proposal by Solomon Feferman to clarify the nature of CH. He has advocated an account of the set-theoretic universe which allows him to distinguish between definite and indefinite mathematical problems. His way of formally regimenting this informal distinction is by employing intuitionistic logic for domains for which one is a potentialist and reserving classical logic for domains for which one is an actualist. This framework allowed him to state a precise conjecture about CH, which has now been proved. I plan to indicate a rough sketch of the proof.
10.00–11.45
Jacopo Emmenegger
A weak factorization system between type theory and homotopy theory
Abstract: Gambino and Garner have proved that the rules of the identity type in Martin-Löf type theory imply the existence of a weak factorization system in the syntactic category, known as the identity type w.f.s. We present a generalization of this result to a category satisfying four axioms reminiscent of the rules of Martin-Löf type theory, and show that it applies also to the category of small groupoids and to that one of topological spaces, giving back the weak factorization systems generated by Grothendieck fibrations and by Hurewicz fibrations, respectively. The categorical setting also highlights a close connection between Paulin-Mohring rules for the identity type and the identity type w.f.s. Some familiarity with dependent type theory and basic homotopy theory will be assumed.
10.00–11.45
Jiri Rosicky, Brno
Towards categorical model theory
Abstract: We will explain how abstract elementary classes are situated among accessible categories and how model theory can be extended from the former to the latter. In particular, we will deal with categoricity, saturation, Galois types and tameness.
10.00–11.45
Aarne Ranta, Göteborg
Machine Translation: Green, Yellow, and Red
Abstract: The main stream in machine translation is to build systems that are able to translate everything, but without any guarantees of quality. An alternative to this is systems that aim at precision but have limited coverage. Combining wide coverage with high precision is considered unrealistic. Most wide-coverage systems are based on statistics, whereas precision-oriented domain-specific systems are typically based on grammars, which guarantee translation equality by some kind of formal semantics.
This talk introduces a technique that combines wide coverage with high precision, by embedding a high-precision semantic grammar inside a wide-coverage syntactic grammar, which in turn is backed up by a chunking grammar. The system can thus reach good quality whenever the input matches the semantics; but if it doesn’t, the user will still get a rough translation. The levels of confidence can be indicated by using colours, whence the title of the talk.
The talk will explain the main ideas in this technique, based on GF (Grammatical Framework) and also inspired by statistical methods (probabilistic grammars) and the Apertium system (chunk-based translation), boosted by freely available dictionaries (WordNet, Wiktionary), and built by a community of over 50 active developers. The current system covers 11 languages and is available both as a web service and as an Android application. (extended version of my talk at Vienna Summer of Logic, http://www.easychair.org/smart-program/VSL2014/NLSR-2014-07-18.html#talk:3396)
10.00–11.45
Peter LeFanu Lumsdaine
Introduction to HoTT, for logicians
Abstract: What is Homotopy Type Theory? Many things! It can be seen as (non-exhaustively):
10.00–11.45
Fredrik Nordvall Forsberg, University of Strathclyde
Inductive-inductive definitions in Intuitionistic Type Theory
Abstract: Martin-Löf’s dependent type theory can be seen both as a foundational framework for constructive mathematics, and as a functional programming language with a very rich type system. Of course, we want this language to have a rich notion of data structure as well. I will describe one class of such data types, where a type A is formed inductively, simultaneously with a second type B : A -> Type which depend on it. Since both types are formed inductively, we call such definitions inductive-inductive definitions. Examples of inductive-inductive definitions — e. g. sorted lists, Conway’s Surreal numbers and the syntax of dependent type theory — will be given, and their meta-theory discussed.
10.00–11.45
Henrik Forssell and Håkon R. Gylterud
Type theoretical databases
Abstract: We present a soundness theorem for a dependent type theory with context constants with respect to an indexed category of (finite, abstract) simplical complexes. From a computer science perspective, the interesting point is that this category can be seen to represent tables in a natural way. Thus the category is a model for databases, a single mathematical structure in which all database schemas and instances (of a suitable, but sufficiently general form) are represented. The type theory then allows for the specification of database schemas and instances, the manipulation of the same with the usual type-theoretic operations, and the posing of queries. This is joint work with David I. Spivak (MIT).
10.00–11.45
Justyna Grudzinska, Warsaw
Generalized Quantifiers on Dependent Types: A System for Anaphora
Abstract: We propose a system for the interpretation of anaphoric relationships
between unbound pronouns and quantifiers. The main technical contribution
of our proposal consists in combining generalized quantifiers with dependent
types. Empirically, our system allows a uniform treatment of all types of
unbound anaphora, including the notoriously difficult cases such as quantificational
subordination, cumulative and branching continuations, and ‘donkey anaphora’.
[This is joint work with Marek Zawadowski.]
13.30–15.15
Marek Zawadowski, Warsaw
Equational Theories for Combinatorics and Geometry
Abstract: Monads, Lawvere Theories, and Operads provide different means to define algebraic structures in categories. Under some natural assumptions they present the same algebraic structures in the category Set. Symmetric operads were originally introduced to study the geometry of loop spaces, whereas analytic and polynomial monads were introduced to study enumerative combinatorics. They have been applied with a success to combinatorial problems related to higher-dimensional categories. In my talk I will discuss the subcategories of categories of monads (on Set) Lawvere theories, and operads (in Set) that correspond to various classes of equational theories relevant for combinatorics and geometry.
Jouko Väänänen, Helsinki
Dependence and independence: A logical approach
Henrik Forssell
Constructive completeness and exploding models
Abstract: We present a unifying categorical approach, based on Joyal’s completeness theorem, that proves constructive completeness theorems for classical and intuitionistic first order logic, as well as for the coherent fragment. We show that the notion of exploding structure introduced by Veldman in 1976 is adequate for certain fragments of first-order logic and that Veldman’s modified Kripke semantics arises, as a consequence, as the semantics of a suitable sheaf topos. The proof, as that of Veldman’s, makes use of the fan theorem. This raises the question of how far one can get in proving completeness constructively but without using the fan theorem. We show that the disjunction-free fragment is constructively complete without appeal to the fan theorem, and also without placing restrictions on the decidability of the theories and the size of the language. Along the way we show how the completeness of Kripke semantics for the disjunction free fragment is equivalent, over IZF, to the Law of Excluded middle. (This is joint work with Christian Espíndola.)
Per Martin-Löf
Sample space-time
Per Martin-Löf
Dependence and causality
Erik Palmgren
On dependently typed first-order logic (cont.)
Abstract: Dependently typed (or sorted) first-order logics were introduced and studied by M. Makkai (1995), P. Aczel and N. Gambino (2006) and J.F. Belo (2008). Belo gave a completeness theorem for an intuitionistic version of such a logic with respect Kripke semantics. In this talk we consider a more general semantics based on categories with families. (This seminar is a continuation from September 18.)
Håkon Robbestad Gylterud
Univalent Multisets
Abstract: Multisets, like sets, consist of elements and the order of appearance of these elements is irrelevant. What distinguishes multisets from sets is the fact that number of occurrences of an element matters. In this talk I will show how one may capture this intuition in Martin-Löf Type Theory. First, I will present a technical result on the identity types of W-types in type theory (without the Univalence Axiom). In light of this result I will give an analysis of the underlying type of Aczel’s model of Constructive Zermelo-Fraenkel set theory (CZF) in presence of the Univalence Axiom. The conclusion is that Aczel’s type, considered with the identity type as equality, consist of iterative, transfinite multisets. I will also present an axiomatic approach to multisets - based on a "translation" of the axioms of CZF.
Peter LeFanu Lumsdaine, IAS, Princeton
Semi-simplicial sets, with an eye to type theory
Abstract: Simplicial sets give, classically, a wonderful model for homotopy theory, and a very satisfying interpretation of type theory. In constructive settings, however, this theory breaks down in several ways. One candidate for repairing it is to pass to *semi-simplicial sets* - structures like simplicial sets, but with only face operations, not degeneracies. These are in some ways harder to work with than simplicial sets, but constructively, they seem much better-behaved. I will show how to construct (classically) a right semi-model structure on semi-simplicial sets, and a resulting model of type theory; and I will discuss the issues involved in attempting to constructivise these results.
Roy T Cook, University of Minnesota
There is No Paradox of Logical Validity
Abstract: A number of arguments have recently appeared (independently in work by Beall & Murzi, Shapiro, and Whittle) for the claim that the logical validity predicate, when added to Peano Arithmetic (PA), is inconsistent in much the same manner as the addition of an unrestricted truth predicate to PA leads to a contradiction. In this paper I show that there is no genuine paradox of logical validity. Along the way a number of rather important, rather more general, lessons arise, including: (i) Whether or not an operator is logical depends not only on what content that operator expresses, but the way that it expresses that content (e.g. as a predicate versus as a logical connective). (ii) Different paradoxes (or purported paradoxes) require different assumptions regarding the status of the principles involved (e.g. mere truth preservation versus logical validity). (iii) A previous analysis of the purported paradox, due to Jeffrey Ketland, fails to properly locate the root of fallacious reasoning involved (apportioning the blame equally to the assumption that PA is logically valid and to the assumption that the validity rules are themselves logically valid). As a result, there is no paradox of logical validity. More importantly, however, these observations lead to a number of novel, and important, insights into the nature of validity itself.
Christian Espíndola
The completeness of Kripke semantics in constructive reverse mathematics
Abstract: We will consider in intuitionistic set theory the completeness theorem with respect to Kripke semantics and analyze its strength from the point of view of constructive reverse mathematics. We will prove that, over intuitionistic Zermelo-Fraenkel set theory IZF, the strong completeness of the negative fragment of intuitionistic first order logic is equivalent, in the sense of interderivability, to (all instances of) the law of the excluded middle, and that the same result holds for the disjunction-free fragment. On the other hand, we will prove that the strong completeness of full intuitionistic first order logic is equivalent, over IZF, to (all instances of) the law of the excluded middle plus the Boolean prime ideal theorem. As a consequence, we will see that the generalization to arbitrary theories of Veldman’s completeness theorem for modified Kripke semantics cannot be proved in IZF. Finally, we will mention aspects of a joint work in progress with Henrik Forssell on the categorical analysis of modified Kripke semantics and how it could be used to derive in IZF completeness proofs for the disjunction-free fragment.
Ali Enayat, Göteborg
Satisfaction classes: conservativity, interpretability, and speed-up
Abstract: This talk reports on joint work with Albert Visser (Utrecht). A full satisfaction class on a model M of PA (Peano arithmetic) is a subset S of M that decides the ‘truth’ of all arithmetical formulae with parameters in M (including those of nonstandard length, if M is nonstandard), while obeying the usual recursive Tarski conditions for a satisfaction predicate. I will present a robust technique for building a wide variety of full satisfaction classes using model-theoretic ideas. This model-theoretic construction lends itself to certain arithmetizations, which in turn can be employed to show that the conservativity of PA + "S is a full satisfaction class" over PA can be verified in Primitive Recursive Arithmetic. I will also comment on the ramifications of the aforementioned arithmetization on interpretability, and speed-up of PA + "S is a full satisfaction class" over PA.
Thierry Coquand, Göteborg
A model of Type Theory in cubical sets
Abstract: We present a model of Type Theory where a type is interpreted as a cubical set satisfying the Kan condition. This can be seen both as a refinement of Bishop’s definition of a set as a collection with an equivalence relation and as a constructive version of Voevodsky’s Kan simplicial set model. We use cubical sets with non ordered dimensions, and explain the connection with the notion of nominal sets. Finally, we show how to use this model to give a new explanation of the axiom of description.
Guillaume Brunerie, Nice
A type-theoretic definition of weak infinity-groupoids
Abstract: The notion of weak infinity-groupoid was originally developed by Grothendieck with the hope of providing an algebraic model for spaces up to homotopy. This notion has also recently come up in type theory with the proof by van den Berg, Garner and Lumsdaine that every type in dependent type theory has the structure of a weak infinity-groupoid (using the definition of Batanin-Leinster). In this talk I will present a type-theoretic definition of the notion of weak infinity-groupoid, equivalent to Grothendieck’s definition, and prove that every type in dependent type theory is such a weak infinity-groupoid.
Henrik Forssell
Localic methods in constructive model theory
Abstract: We outline some preliminary investigations into using locale-theoretic methods in constructive model theory, methods springing from such results as the sheaf-theoretic representation and cover theorems of Joyal and Tierney and (formal) space valued completeness theorems of e.g. Coquand and Smith.
Dag Prawitz
Relations between Gentzen’s and Heyting’s approaches to meaning
Erik Palmgren
On dependently typed first-order logic
Per Martin-Löf
Truth of empirical propositions
Mateus de Oliveira Oliveira
The parameterized complexity of equational logic
Abstract. We introduce a variant of equational logic in which sentences are pairs of the form (s=t, ω) where ω is an arbitrary ordering of the sub-terms appearing in s=t. To each ordered equation (s=t, ω) one may naturally associate a notion of width, and to each derivation of an ordered equation (s=t, ω) from a set of axioms E, one may naturally define a notion of depth. The width of such a derivation is defined as the width of the thickest ordered equation appearing in it. Our main result states that for any fixed set of axioms E and constants c and d one may determine whether a given ordered equation (s=t, ω) can be inferred from E in depth d and width c in time f (|E|, d, c)*|s = t|^O(c) . Additionally we will define the notion of b-bounded substitution. We say that a proof is b- bounded if every substitution rule used on it is b-bounded. We will show that one may determine whether (s=t, ω) follows from E via a b-bounded proof of depth d and width c in time f (|E|, d, c, b)|s = t|.
Simone Tonelli
Investigations into a model of type theory based on the concept of basic pair. (Presentation of MSc Thesis)
Abstract. he principal aim of this thesis is to explain a possible model of Per Martin-Löf’s type theory based on the concept of Giovanni Sambin’s basic pair. This means to extend the concept of "set" in the easiest and most natural way: transforming it in a couple of sets and an arbitrary relations set between them, i.e. a basic pair. This reasoning will be applied to all the judgment forms and will give us an interpretation of Martin-Löf’s type theory. Our purpose will be to find a model which satisfies this interpretation, and we will look for it following two different approaches. The first one is meant to remain inside the standard type theory constructing an internal model; the second one, arisen from some impasses reached in the development of the first attempt, is aimed at adding new type constructors at the standard theory, extending it and allowing us to create an external model. These new types, that we have denoted here with a star, have to be seen like an arbitrary relations set between two set of the same type without star. This extended theory will give us all the results needed in a natural way, and might be useful in different interpretations for further research.
Douglas Bridges (University of Canterbury, Christchurch, New Zealand)
TBA in Constructive Theory of Apartness Spaces
Abstract. The theory of apartness spaces, a counterpart of the classical one of proximity spaces, provides one entry to a purely constructive (i.e. developed with intuitionistic logic and CZF set theory or ML type theory) study of topology. The canonical example of apartness spaces are metric spaces, locally convex spaces, and, more generally, uniform spaces. The general theory of apartness and its specialisation to uniform spaces has been studied extensively since 2000, and is expounded in detail in [1]. In this talk we first present the basic notions of apartness between sets and of uniform structures, and point out the connection between point-set apartness spaces and neighbourhood spaces. We then introduce u-neighbourhood structures, which lie somewhere between topological and uniform neighbourhood structures. It turns out that every reasonable apartness space $X$ has an associated apartness relation $\bowtie _{w}$ induced by a u-neighbourhood structure. Classically, that associated structure is induced by the unique totally bounded uniform structure that induces the original apartness on $X$. Although there is no possibility of proving, in general, that $\bowtie _{w}$ is induced constructively by a uniform structure, it is always induced by a u-neighbourhood structure. The mysterious ‘TBA’ in the title of the talk derives from the fact that there is a natural definition of total boundedness for u-neighbourhood spaces, enabling us to examine the computationally useful notion of totally bounded apartness (TBA) outside the context of a uniform space. Reference [1] D.S. Bridges and L.S.V\^{\i}\c{t}\u{a}, Apartness and Uniformity: A Constructive Development, in: CiE series Theory and Applications of Computability, Springer Verlag, Heidelberg, 2011.
André Porto (Universidade Federal de Goiás, Brazil)
Rules, Equations and Infinity in Wittgenstein
Abstract: Our presentation will address Wittgenstein’s construal of different kinds of mathematical statements, such as singular and general equations, with special attention to his handling of the notion of infinity. We will argue for a close proximity between his proposals and those of Category Theory. We will also pay close attention to the differences between his elucidations and the ones offered by contemporary Intuitionism.
Erik Palmgren
The Grothendieck construction and models for dependent types
Per Martin-Löf
Invariance under Isomorphism and Definability (continued)
Per Martin-Löf
Invariance under Isomorphism and Definability (continued)
Per Martin-Löf
Invariance under Isomorphism and Definability
Christian Espíndola
On Glivenko theorems for intermediate predicate logics
Abstract: We will expose a simple proof-theoretic argument showing that Glivenko’s theorem for propositional logic and its version for predicate logic follow as an easy consequence of the deduction theorem, from which we will show with the same elementary arguments some Glivenko-type theorems relating intermediate logics between intuitionistic and classical logic. We will consider two schemata, the double negation shift (DNS) and the one consisting of instances of the principle of excluded middle for sentences (REM). We will prove that both schematas combined derive classical logic, while each one of them provides a strictly weaker intermediate logic, and neither of them is derivable from the other. We will show that over every intermediate logic there exists a maximal intermediate logic for which Glivenko’s theorem holds, and also deduce two characterizations of DNS, as the weaker (with respect to derivability) schema that added to REM derives classical logic and as the strongest (with respect to derivability) schema among the ¬¬-stable ones.
Håkon Robbestad Gylterud
The partiality monad and its algebras
Abstract: In this talk I will give a description of the partiallity monad, its implementation in Martin-Löf type theory, and talk about my current research into its properties. The partiality monad is an attempt to give an abstract descriptions of what a computation is, using categorical language. From any monad we can construct its Kleisli category, and in the case of the partiallity monad the Kleisli category models partial, computable functions. I have begun an investigation into how this monad can be used to describe some aspects of computability in Martin-Löf type theory. I will relate this to other approaches to constructive computability theory (in particular Richman’s "Church’s thesis without tears"), and talk about the algebras for this monad and their connections to domain theory.
Allard M. Tamminga, Bayreuth and Groningen
Correspondence analysis for many-valued logics (joint work with Barteld Kooi)
Abstract: Taking our inspiration from modal correspondence theory, we present the idea of correspondence analysis for many-valued logics. As a benchmark case, we study truth-functional extensions of the Logic of Paradox (LP). First, we characterize each of the possible truth table entries for unary and binary operators that could be added to LP by an inference scheme. Second, we define a class of natural deduction systems on the basis of these characterizing inference schemes and a natural deduction system for LP. Third, we show that each of the resulting natural deduction systems is sound and complete with respect to its particular semantics.
Peter Schuster, Pure Mathematics, University of Leeds
When Irreducibles are Prime
Abstract: Many an indirect proof with Zorn’s Lemma has recently allowed for being turned upside down into a direct proof with Raoult’s Open Induction; case studies pertain to commutative rings [1] and Banach algebras [2]. Under sufficiently concrete circumstances this may even yield a constructive proof without any form of the Axiom of Choice. To prepare the ground for a more systematic treatment we now classify the cases that can be found in mathematical practice by way of representative proof patterns. To start with we distill, and prove by Open Induction, a generalised form of the contrapositive of the Separation Lemma or Prime Ideal Theorem that is ascribed to Lindenbaum, Krull, Stone, and Tarski. Our version subsumes not only instances from diverse branches of abstract algebra but also a Henkin-style completeness proof for first-order logic. By recurrence to a theorem of McCoy, Fuchs, and Schmidt on irreducible ideals we further shed light on why prime ideals occur — and why transfinite methods. (This is joint work in progress with D. Rinaldi, Munich, and is partially based on joint work with N. Gambino, Palermo, and F. Ciraulo, Padua.)
[1] P. Schuster, Induction in algebra: a first case study. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 2012, Dubrovnik, Croatia. IEEE Computer Society Publications (2012) 581-585
[2] M. Hendtlass, P. Schuster, A direct proof of Wiener’s theorem. In: S.B. Cooper, A. Dawar, B. Loewe, eds., How the World Computes. Turing Centenary Conference and 8th Conference on Computability in Europe, CiE 2012, Cambridge, UK, June 2012, Proceedings. Springer, Berlin and Heidelberg. Lect. Notes Comput. Sci. 7318 (2012) 294-303
Tero Tulenheimo, University of Lille
Classical Negation and Game-Theoretical Semantics
Abstract: Typical applications of Hintikka’s game-theoretical semantics (GTS) give rise to semantic attributes — truth, falsity — expressible in the \Sigma^1_1 fragment of second-order logic. Actually a much more general notion of semantic attribute is motivated by strategic considerations. When identifying such a generalization, the notion of classical negation plays a crucial role. We study two languages, L_1 and L_2, in both of which two negation signs are available: \neg and \sim. The latter is the usual GTS negation which transposes the players’ roles, while the former will be interpreted via the notion of {\it mode}. Logic L_1 extends IF logic; \neg behaves as classical negation in L_1. Logic L_2 extends L_1 and it is shown to capture the \Sigma^2_1 fragment of third-order logic. Consequently the classical negation remains inexpressible in L_2.
13.00–14.45, room 306, building 6, Kräftriket, Stockholm (Note: time and place)
Henrik Forssell, University of Oslo
Title: Simplicial databases
Abstract: We consider a database model based on (finite) simplicial complexes rather than relations. A brief introduction to the relational model is given for logicians not familiar with it. We thereafter describe how simplicial complexes can be used to model both database schemas and instances. This allows us to collect schemas and instances over them into one structure, which we relate to the notions of display map and comprehension category.
Benno van den Berg, Utrecht University
Title: Predicative toposes
Abstract: Topos theory is a very successful chapter in the categorical analysis of logic. Elementary toposes are categorical models of higher-order intuitionistic arithmetic and provide a framework for almost all interpretations of this theory, such as realizability, Kripke , topological and sheaf models. The notion of a topos is impredicative, however, and therefore its internal logic is much stronger than what most constructivists are willing to use in their work. Indeed, most constructivists want their work to be formalisable in weaker predicative systems like Martin-Lof’s type theory and Peter Aczel’s constructive set theory CZF. A predicative topos should be a topos-like structure whose internal logic has the same strength as these theories. I will explain what the difficulties are in coming up with a good notion of predicative topos, discuss two possible axiomatisations (very closely related), explain why I like these and then discuss their basic properties.
Erik Palmgren
Survey of notions of models for dependent type theories
Abstract: The notion of a model of Martin-Löf type theory, or more general dependent type theories, is fairly complicated and exists in several versions. We give a survey of some of the most important ones.
Peter Dybjer (Chalmers)
Tests, games, and Martin-Löf’s meaning explanations for intuitionistic type theory
Abstract: In this talk I shall argue that program testing provides the basis for constructive mathematical truth. This point of view leads to an alternative presentation of Martin-Löf’s meaning explanations for intuitionistic type theory, where the judgements of type theory are viewed as conjectures which can be tested in order to be corroborated or refuted. In particular, we get a new interpretation of hypothetical judgments, since tests for such judgments need methods for generating inputs. We sketch a "test manual" for intuitionistic type theory which employs concepts from game semantics, for example, input generation corresponds to opponent’s moves in a game. In order to test a typing judgement we simultaneously play a strategy generated by a type and a strategy generated by a term, where the correct moves for the strategy of the term are determined dynamically by playing the strategy of the type.
The talk is on joint work in progress with Pierre Clairambault, Cambridge.
Dag Westerståhl
Compositionality in context
Abstract: The standard notion of compositionality is well understood, and the formal framework of Hodges (2001) allows precise treatment of various features of compositionality. The issue in this talk is how context-dependence, i.e. cases where semantic values are assigned to syntactic expressions *in contexts*. Contexts here can be assignments, utterance situations (or features thereof s.a. speakers, times, locations, possible worlds,...), standards of precision, etc., or various aspects of linguistic context. Currying the context argument results in a function taking only expressions as arguments, and one question concerns the relation between compositionality of the curried function and that of the uncurried one. Another question is the relation between a compositional semantics and one given by a standard inductive truth definition. The background to these questions is linguistic, but in this talk I focus on the mathematical details.
Sam Sanders, Ghent University
Reuniting the antipodes: bringing together Constructive and Nonstandard Analysis
Abstract: In the Sixties, Errett Bishop introduced Constructive Analysis, a redevelopment of classical Mathematics based on the fundamental notions of ‘algorithm’ and ‘proof’, inspired by the BHK (Brouwer-Heyting-Kolmogorov) interpretation. Constructive Reverse Mathematics (CRM) is a spin-off from Harvey Friedman’s famous ‘Reverse Mathematics’ program, based on Constructive Analysis. Bishop famously derided Nonstandard Analysis for its lack of computational meaning. In this talk, we introduce ‘Ω-invariance’: a simple and elegant definition of ‘finite procedure’ in (classical) Nonstandard Analysis. Using an intuitive interpretation, we obtain many results from CRM, thus showing that Ω-invariance is quite close to Bishop’s notion of algorithm. We suggest a possible application of Ω-invariance to Per Martin-Löf’s famous Type Theory, in light of its recent interpretation using homotopy.
Henrik Forssell, Oslo
Recovering theories from their models
Abstract: Given a theory T and its category of models and homomorphisms Mod(T), is it possible to recover T from Mod(T) (up to some suitable notion of equivalence)? A positive answer for regular theories was given by Makkai who showed that the classifying topos of a regular theory - from which the theory can be recovered - can be represented as filtered colimit preserving functors from Mod(T) to the category SET of sets and functions. Moving to coherent (and classical first-order theories), however, it becomes necessary to equip Mod(T) with some extra structure. While Makkai uses structure based on ultra-products for this case, it is possible to equip Mod(T) with a natural topology and represent the classifying topos of T as equivariant sheaves on the resulting topological category (or groupoid, considering just the isomorphisms). This forms the basis of an extension of Stone duality to first-order theories, and allows for the application of topos-theoretic techniques to e.g. give a topological characterization of the definable subclasses of Mod(T).
Juha Kontinen, Helsinki
Axiomatizing first-order consequences in dependence logic
Abstract: Dependence Logic, introduced by Jouko Väänänen in 2007, is a new logic incorporating the concept of dependence into first-order logic. The expressive power of dependence logic coincides with that of existential second-order logic In the past few years, dependence logic has grown into a new framework in which various notions of dependence and independence can be formalized. The high expressive power of dependence logic has a consequence that dependence logic in full generality cannot be axiomatized. However, first-order consequences of dependence logic sentences can be axiomatized. We give an explicit axiomatization and prove the respective Completeness Theorem. This is joint work with Jouko Väänänen.
Hajime Ishihara (Japan Advanced Institute of Science and Technology)
Some Conservative Extension Results of Classical Logic over Intuitionistic Logic
Erik Palmgren
What is an internal setoid model of dependent type theory?
Abstract: Standard models of dependent type theory, such as categories with attributes, use semantics based on the category of sets. It seems to be an unresolved question how to best formulate such semantics using the category of setoids instead, and how to do this internally to type theory it self. We discuss some proposals for solutions and possible generalizations to other categories of interpretation.
Peter Schuster (Leeds)
A Proof Pattern in Algebra
Abstract: Many a concrete theorem of abstract algebra admits a short and elegant proof by contradiction but with Zorn’s Lemma. A few of these theorems have recently turned out to follow in a direct and elementary way from Raoult’s Principle of Open Induction, a little known equivalent of Zorn’s Lemma. A proof of the latter kind typically follows a certain pattern, and may be extracted from a proof of the former sort. If the theorem has finite input data, then a finite order carries the required instance of induction, which thus is provable by fairly elementary means. Basic proof theory suffices to eliminate the decidability assumptions one may have to make en route. The tree one can grow alongside the induction encodes an algorithm which computes the desired output data. We will discuss all this along the lines of some typical examples.
13.15–15.00, room 16, building 5, Kräftriket, Stockholm. (Note time and day!)
Mohammad Jabbari (SU)
Algebraic Theories and Algebraic Categories
Abstract: Algebra is a subject dealing with variables, operations and equations. This viewpoint - present in the Tarski-Birkhoff’s tradition in universal algebra - was the scene before the birth of categorical logic in F. W. Lawvere’s 1963 thesis. In his thesis, among other things, he objectified algebraic "theories" as special kind of categories and algebraic structures as special set-valued functors on them. He learned to do universal algebra by category theory! This was the start of a fruitful line of discoveries which culminated in the creation of (elementary) topos theory by Lawvere and M. Tierney in late 1970.
At about the same time, an alternative categorical approach to general algebra emerged out of the collective efforts of some homological algebraists (Godement, Huber, Eilenberg, Beck, ...) which centers around the notion of "monads (triples)". Among other intuitions, this machinery enables us to grasp the algebraic part of an arbitrary category. This approach later found applications in descent theory and computer science. The highpoint of this area is Beck’s monadicity theorem.
This seminar is divided into three parts. At first we review some of Lawvere’s ideas in algebraic theories and state his characterization theorem for algebraic categories. Then we shortly describe the monadic approach to algebra. Finally we state some theorems about the equivalences between these three approaches into algebraic categories.
Main References.
[1] Lawvere, F. W., "Functorial semantics of algebraic theories", PhD Thesis, Columbia, 1963.
[2] Adamek, J., et al., "Algebraic Theories - A Categorical Introduction to General Algebra", Cambridge University Press, 2011.
Martin Blomgren (KTH)
Essentially small categories
Abstract. To each small category it is possible to associate a homotopy type. This is done through the nerve functor; via this functor it is thus possible to transport homotopy notions from simplicial sets (or topological spaces) to the category of small categories.
In this talk we introduce the notion of essentially small categories; such a category, albeit "big", allows for a nerve construction — an essentially small category has a small subcategory that serves as a good homotopy approximation for its ambient category; we give several concrete examples of "big" but essentially small categories and their homotopy types. We also explain how to do categorical homotopy theory on "big" categories in general.
Christian Espíndola (SU)
Categorical methods in model theory
Abstract. In this talk we will discuss applications of methods in categorical logic to model theory, which was the theme of my undergraduate thesis. In the first part we will expose Joyal’s categorical proof of Gödel’s completeness theorem for first order classical logic, which is based on a series of unpublished lectures in Montréal in 1978. The proof makes use of functorial semantics, as introduced by Lawvere, to translate into categorical language the existing proof of completeness. In the second part we will make use of Joyal’s constructions and explain how they can be adapted to give categorical proofs of Löwenheim-Skolem theorem and of the criterion known as Vaught’s test, which gives sufficient conditions for a first order theory to be complete. We will also comment on the constructive aspects of the categorical proofs, as well as to what extent they can dispense with choice principles.
Dag Prawitz
Gentzen’s 2nd consistency proof and normalization of natural deductions in 1st order arithmetic
Håkon Robbestad Gylterud (SU)
Symmetric Containers
Abstract. This talk is based on my Master Thesis. I will give a brief introduction to the notion of a container and how to differentiate them, as defined in [1] and [2]. This yields combinatorial information from the process of differentiation (a la combinatorial species). Then I show how a more general notion, called symmetric containers, contains anti-derivatives of many containers.
References
[1] Michael Abbott, Thorsten Altenkirch and Neil Ghani (2005). Containers: constructing strictly positive types, Theoretical Computer Science 342(1), 3 - 27.
[2] Michael Abbott, Thorsten Altenkirch, Neil Ghani and Conor Mcbride (2008), ∂ for data: Differentiating data structures.
Douglas S. Bridges, University of Canterbury,
Christchurch, New ZealandApproaching topology constructively via apartness
Abstract: In 2000, Luminita Vita and I began investigating axioms for a constructive theory of apartness between points and sets, and between sets and sets, as a possible constructive approach to topology. The culmination of this work came last October, with the publication of the monograph [3], in which we lay down what we believe to be the defnitive axioms for (pre-)apartness and then develop the theory, with particular application to (quasi-)uniform spaces. Our development uses points, and is therefore in the style and spirit of Bishop’s original constructive approach to analysis [1, 2]. As with analysis, so with topology: once the "right" axioms are used, the theory allows in a natural, if technically nontrivial, way (with one exception). In this talk I shall present the axioms for apartness and uniform spaces, and discuss various aspects of the resulting theory, paying particular attention to the connections between various types of continuity of functions.
References
[1] E. Bishop, Foundations of Constructive Analysis, McGraw-Hill, New York 1967.
[2] E. Bishop and D.S. Bridges, Constructive Analysis, Grundlehren der Math. Wissenschaften 279, Springer Verlag, Heidelberg, 1985.
[3] D.S. Bridges and L. Vita, Apartness and Uniformity: A Constructive Development, in: CiE series "Theory and Applications of Computability", Springer Verlag, Heidelberg, 2011.
Minisymposium on categorification and foundations of mathematics and quantum theory
Room 16, building 5, Kräftriket, Stockholm.
9.15–10.05: Bas Spitters (Radboud University, Nijmegen)
Bohrification: Topos theory and quantum theory
Abstract. Bohrification associates to a (unital) C*-algebra
10.15–11.05: Thierry Coquand (Göteborg)
About the Kan simplicial set model of type theory
11.15–12.05: Volodymyr Mazorchuk (Uppsala)
2-categories, 2-representations and applications
Abstract. In this talk I plan to explain what a 2-category is, how 2-categories appear in algebra and topology, how one can study them, in particular, how one constructs 2-representations of 2-categories, and, finally, how all this can be applied.
13.30–14.20: Erik Palmgren (Stockholm)
Proof-relevance of families of setoids and identity in type theory
Abstract. Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A similar result is shown for fibre representations of families. The ubiquitous role of proof-irrelevant families is discussed.
14.30–15.20: Nils Anders Danielsson (Göteborg)
Bag equality via a proof-relevant membership relation.
Abstract. Two lists are "bag equal" if they are permutations of each other, i.e. if they contain the same elements, with the same multiplicity, but perhaps not in the same order. I will describe how one can define bag equality as the presence of bijections between sets of membership proofs. This definition has some nice properties:
Dag Westerståhl
Logical constants and logical consequence
Abstract: I will first briefly overview the problem of logical constants (what is it that makes a symbol logical?) and some approaches to it, in particular the invariance approach originating with Tarski. Then I present some recent joint work with Denis Bonnay on a new approach: Given an interpreted language and a set of logical constants, Tarski’s semantic definition of logical consequence yields a consequence relation. But given a consequence relation, is there a natural way to extract from it a set of logical constants? I compare two ways of doing so, one purely syntactical, based on the idea that an expression is logical if it is essential to the validity of at least one inference, and one semantical, based on the idea that an expression is logical if its interpretation is fully determined by the rules for its use. To describe these methods, Galois connections between consequence relations, sets of symbols, and sets of interpretations (all ordered under inclusion) play an important role.
Erik Palmgren
Voevodsky’s foundations - type-theoretic background and the univalence axiom
Abstract: This talk is the second in a series around Voevodsky’s proposal for a novel foundations of mathematics based on notions from homotopy theory. We shall here present some background in Martin-Löf type theory, in particular pertaining to the identity types which are central to the approach, giving the notion of path. Furthermore the Univalence Axiom and its consequences are discussed. If time permits we also start presenting Voevodsky’s standard model of type theory extended with this axiom.
Torsten Ekedahl
Voevodsky’s foundations - homotopy and categorical background
Abstract: I will give some background in homotopy and category theory that should aid in understanding Voevodsky’s proposed approach to the foundations of type theory. This includes how groupoids and n-groupoids appear naturally as a framework for equality when one wants to retain as much information as possible but also how homotopy and in particular homotopy coherence comes into the picture.
Three lecture seminar series in theoretical computer science & mathematical logic
Containers, a mini-course
Prof. Neil Ghani, University of Strathclyde, UK
Summary: The semantics of data types within computer science is often given using initial algebra semantics. However, not all functors have initial algebras and even those that do often lack good properties. As a result, a number of formalisms have been invented to capture those functors which give rise to initial algebras with good properties. Containers are one such formalism and this series of talks concerns them. One of the pleasant features I will mention is the smooth generalisation of containers to indexed containers and then to inductive recursive definitions. I’ll aim to make my talks accessible to those with an understanding of one of i) category theory; ii) type theory; or iii) functional programming.
Andrew Pitts, Cambridge
Structural Recursion with Locally Scoped Names
Abstract: I will discuss a new recursion principle for inductive data modulo alpha-equivalence of bound names that makes use of Odersky-style local names when recursing over bound names. It is inspired by the nominal sets notion of "alpha-structural recursion". The new approach provides a pure calculus of total functions that still adequately represents alpha-structural recursion while avoiding the need to verify freshness side-conditions in definitions and computations. It arises from a new semantics of Odersky-style local names using nominal sets.
Ogawa Mizuhito, JAIST, Japan
Confluence of Term Rewriting Systems, brief history and recent progress
Abstract: Confluence and termination are two major target properties of rewrite systems. This talk briefly overviews the histroy of sufficient conditions for confluence of first-order term rewriting systems, and recent progress from our group will be introduced. (One appeared in IJCAR this July and another will come soon in IPL.)
Erik Palmgren
On the category of types with intensional identity
Per Martin-Löf
Contexts and cubical complexes
Johan Glimming
Towards Parametric Direcursion
Peter Dybjer, Chalmers
The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theory with Pi, Sigma, and Extensional Identity Types
Abstract: In his paper Locally cartesian closed categories (1984) and type theory Robert Seely presented a proof that the category LCC of locally cartesian closed categories and the category ML of syntactically presented Martin-Löf type theories (with Pi, Sigma, and extensional identity types) are equivalent. However, Seely’s proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks in categories. In his paper "Substitution up to isomorphism" Curien (1993) shows that Seely’s problem is essentially a coherence problem and proposed how to solve this problem using cut-elimination. An alternative interpretation was then proposed by Hofmann (1994) based on a method due to Benabou. However, neither Curien nor Hofmann showed that their respective interpretations lead to an equivalence between LCC and ML. In this paper we show that Hofmann’s interpretation functor gives rise to a biequivalence of 2-categories, and claim that this is the appropriate formulation of Seely’s theorem. We replace ML with a categorical analogue CWFLCC of categories with families (with extensional identity types, and Sigma and Pi-types) which are democratic in the sense that each context is represented by a closed type. Most of the difficulty of this proof already appears when relating categories with finite limits (without assuming local cartesian closure) and categories with families without Pi-types. We therefore present this biequivalence (of the 2-categories FL and CWFFL) separately. (Joint work with Pierre Clairambault, PPS, Paris 7)
Johan Granström
Metamodelling in constructive type theory
Abstract: Denotational semantics of programming languages often involve recursive function spaces in the domain equation, and for such Freyd proposed a recursion scheme, called direcursion, which allows definition and proofs, as studied also in the work of Pitts. We will in this paper generalise this mixed-variant recursion scheme and show that it can be parameterised by an adjunction equipped with two natural transformations that distribute the functors of the adjunction in a certain sense over the domain constructors, generalising strength for endofunctors to the mixed-variant situation. This gives also a generalisation of enrichment of an endofunctor to the situation of mixed-variant functors. The new recursion scheme, called parametric direcursion, solves the problem of maintaining additional arguments while computing with recursive types. Applications are anticipated in the area of object-based programming languages and ormalisation-by-evaluation for untyped lambda calculus (work in progress).
Richard Garner
Ionads and constructive topology.
Abstract: Formal topology provides a way of defining topological structures within constructive type theory. However, the theory of formal topologies is more akin to that of locales than to that of topological spaces. The purpose of this talk is to discuss a way in which the theory of topological spaces could be embedded directly into constructive type theory; it employs a new notion—that of an ionad—which may be seen as a proof-relevant generalisation of the notion of topological space.
Douglas S Bridges
Constructive reverse mathematics
Abstract: Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Constructive reverse mathematics is reverse mathematics carried out in Bishop-style constructive math (BISH)—that is, using intuitionistic logic and, where necessary, constructive ZF set theory; see (Bridges and Vita 2006). There are two primary foci of constructive reverse mathematics: first, investigating which constructive principles are necessary to prove a given constructive theorem; secondly, investigating what non-constructive principles are necessary additions to BISH in order to prove a given non-constructive theorem. I will present work on constructive reverse mathematics, carried out with Josef Berger and Hannes Diener. The main theme of the talk is the connection between the antithesis of Specker’s theorem, various continuity properties, versions of the fan theorem, and Ishihara’s principle BD-N.
References
Anton Hedin
Vitali’s covering theorem in constructive mathematics
Abstract: Vitali’s covering Theorem states in its simplest form that if a closed interval I, in the real numbers, is (Vitali-) covered by a collection of open intervals V, then for every k>0 there is a finite subset F of V of pairwise disjoint intervals which cover all of I except a subset of measure less than k. We show that the Theorem fails in Bishop’s constructive mathematics by giving a recursive counterexample. In fact it is equivalent to Weak Weak König’s Lemma over BISH. Moreover we show that, under a reasonable interpretation of Vitali covering, the Theorem holds in the topology of reals in formal topology. The relation to the point-set result is explained via the concept of spatiality of formal topologies. The talk is based on joint work with Dr. Hannes Diener.
Per Martin-Löf
Spreads and choice sequences in type theory (cont.)
Per Martin-Löf
Spreads and choice sequences in type theory (cont.)
Per Martin-Löf
Spreads and choice sequences in type theory
Kim Solin
Applications of modified semirings
Abstract: In this talk I present some applications of semirings that have been modified to serve a particular purpose. These applications include reasoning about programs and reasoning about epistemic notions. I conclude by presenting two open problems.
Sten-Åke Tärnlund
P vs NP
Maintainer: Brandon Doherty, brandon.doherty@math.su.se