WG6 kickoff meeting: Syntax and Semantics of Type Theories — Programme
Overview — Social activities — Abstracts — Meeting homepage
Overview
All talks will take place in room 14, house 5, at Kräftriket (map).
Friday 20 May
 9.30–10.30: Jonathan Sterling, Naïve logical relations in synthetic Tait computability
 10.30–10.50: coffee/tea break
 10.50–11.10: Steve Awodey, KripkeJoyal forcing for MartinLöf type theory
 11.10–11.30: Niels Van der Weide, Semantics for twodimensional type theory
 11.30–11.50: David Wärn, Effective quotients in homotopy type theory

11.50–12.10:
Roussanka Loukanova,
SyntaxSemantics of Simply Typed Theory of Acyclic Algorithms(cancelled)  12.10–13.40: lunch break (Proviant)
 13.40–14.40: Andrej Bauer, One syntax to rule them all
 14.40–15.00: Maximilian Doré, Automating Kan composition
 15.00–15.20: Kenji Maillard, The multiverse — Logical modularity for proof assistants
 15.20–15.50: coffee/tea break
 15.50–16.10: Iosif Petrakis, Positive negation in constructive mathematics
 16.10–16.30: Raffael Stenzel, Higher geometric sheaf theories
 16.30–17.30: Anja Petković Komel, The essence of elaboration
Saturday 21 May
 10.00–11.00: András Kovács, Typetheoretic signatures for algebraic theories and inductive types
 11.00–11.20: coffee/tea break
 11.20–12.20: Théo Winterhalter, MetaCoq: Sound and complete type checking for Coq, in Coq
 12.20–14.00: lunch break (downtown)
 14.00–15.00: Taichi Uemura, Normalization for initial spacevalued models of type theories
 15.00–15.20: Jonas Frey, Characterizing clanalgebraic categories
 15.20–15.40: Jacopo Emmenegger, Bsystems and Csystems are equivalent
 15.40–16.00: coffee/tea break
 16.00–16.20: Sergei Soloviev, Consequences of Computational Asymmetry in VerifierFalsifier Games
 16.20–16.40: Henning Basold, Towards behavioural types as coalgebras
 16.40–17.40: Ivan Di Liberti, Bipresentable 2categories and (bilex) 2sketches
 19.00: dinner at Shahrzad — details below
Social activities
The workshop dinner is 19:00 at Shahrzad, a classic Persian restaurant, 30mins walk from Kräftriket (or 10mins bus + 10 mins walk). We have a prebooked set menu at 500kr/person (drinks not included), with alternatives available for dietary restrictions.
On Sunday, there will be an informal social excursion — not highly organised, mainly just a gatheringpoint to start off together. If the weather is nice, we will go to Skansen, an openair museum of Swedish culture and history (entrance 200kr); if it’s rainy we’ll go to Moderna Museet/ArkDes, a museum of modern art, architecture, and design (main collections free entry, some exhibitions charge entry). Both options have good cafés for lunch/snacks, and other sightseeing nearby. In either case, this is; meet at 11:00 at the main entrance (of Skansen or Moderna Museet), and take things informally from there. We’ll announce which it is on Saturday evening!
Abstracts
Friday 20 May
9.30–10.30: Jonathan Sterling (Aarhus University), Naïve logical relations in synthetic Tait computability
Logical relations are the main tool for proving positive properties of logics, type theories, and programming languages: canonicity, normalization, decidability, conservativity, computational adequacy, and more. Logical relations combine pure syntax with nonsyntactic objects that are parameterized in syntax in a somewhat complex way; the sophistication of possible parameterizations makes logical relations a tool that is primarily accessible to specialists. In the spirit of Halmos’ book Naïve Set Theory, I advocate for a new viewpoint on logical relations based on synthetic Tait computability, the internal language of categories of logical relations. In synthetic Tait computability, logical relations are manipulated as if they were sets, making the essence of many complex logical relations arguments accessible to nonspecialists.
10.50–11.10: Steve Awodey (Carnegie Mellon University), KripkeJoyal forcing for MartinLöf type theory •
I will report on recent joint work with Nicola Gambino and Sina Hazratpour, generalizing the KripkeJoyal forcing semantics of topos theory from IFOL and IHOL to MLTT, contained in the paper arXiv:2110.14576.
11.10–11.30: Niels Van der Weide (Radboud University), Semantics for twodimensional type theory •
In this work, we propose a general notion of model for twodimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature. From comprehension bicategories, we extract a core syntax, that is, judgment forms and structural inference rules, for a twodimensional type theory. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library. This work is the first step towards a theory of syntax and semantics for higherdimensional directed type theory.
11.30–11.50: David Wärn (University of Gothenburg), Effective quotients in homotopy type theory
For a type X, one expects that surjections from X correspond to ‘higher equivalence relations’ on X. A priori this idea is difficult to express internally to type theory since it involves an infinite tower of coherences. In this talk, we give an internal definition of higher equivalence relations and show it to be equivalent to surjections out of X. As an application we obtain a simple proof of the stabilisation theorem for higher groups.
11.50–12.10:
Roussanka Loukanova (Bulgarian Academy of Sciences), SyntaxSemantics of Simply Typed Theory of Acyclic Algorithms (cancelled)
In 1989, Moschovakis [1] initiated a new theory of the mathematical notion of algorithm, within untyped, full recursion. In 2006, Moschovakis [2] introduced the formal language of higherorder TypeTheory of Acyclic Algorithms (TTAR) via simple types, which models the notion of algorithm and concepts of meaning in simplytyped semantic structures. The focus of [2] is on computations that end up after finite number of steps. The approach, in its varieties, with full and acyclic recursion, provides for new developments of type theory of computation and new applications to computational syntaxsemantics interfaces in programing and natural languages.
In this talk, I present the formal language (LAR) of TTAR, by extending it with a restrictor operator that sets conditions on denotations of terms. In addition, the operator defines restricted memory and parameters. TTAR provides two kinds of semantics of the formal language LAR, denotational and algorithmic. The reduction system of TTAR is essential for the notion of algorithm and syntaxsemantics interfaces. I shall overview the reduction calculus and some of the theoretical results of TTAR.
 Yiannis N Moschovakis. The formal language of recursion. Journal of Symbolic Logic, 54(04):1216–1252, 1989.
 Yiannis N. Moschovakis. A Logical Calculus of Meaning and Synonymy. Linguistics and Philosophy, 29(1):27–89, 2006.
13.40–14.40: Andrej Bauer (University of Ljubljana), One syntax to rule them all • blog post & formalisation
The raw syntax of a type theory, or more generally of a formal system with binding constructs, involves not only free and bound variables, but also metavariables, which feature in inference rules. Each notion of variable has an associated notion of substitution. A syntactic translation from one type theory to another brings in one more level of substitutions, this time mapping typetheoretic constructors to terms. Working with three levels of substitution, each depending on the previous one, is cumbersome and repetitive. One gets the feeling that there should be a better way to deal with syntax.
In this talk I will present a relative monad capturing higherrank syntax which takes care of all notions of substitution and bindingpreserving syntactic transformations in one fell swoop. The categorical structure of the monad corresponds precisely to the desirable syntactic properties of binding and substitution. Special cases of syntax, such as ordinary firstorder variables, or secondorder syntax with variables and metavariables, are obtained easily by precomposition of the relative monad with a suitable inclusion of restricted variable contexts into the general ones. The metatheoretic properties of syntax transfer along the inclusion.
The relative monad is sufficiently expressive to give a notion of intrinsic syntax for simply typed theories. It remains to be seen how one could refine the monad to account for intrinsic syntax of dependent type theories.
This is joint work with Danel Ahman from the University of Ljubljana.
14.40–15.00: Maximilian Doré (University of Oxford), Automating Kan composition •
Cubical type theory offers a new of conducting topological arguments with its builtin Kan composition. Constructing a cube with Kan composition amounts to constructing a higher cube with appropriate boundaries, which is a very combinatorial task amenable to automation. In this talk I want to discuss recent work on doing this with the wellknown algorithmic technique of constraint satisfaction. If we want to construct an ndimensional cube as the top lid of a (n+1)dimensional cube, we can solve a constraint satisfaction problem (CSP) with 2n+1 variables, the domains of which are all ncubes which have a boundary matching with the lid. The constraints represent that the boundaries of all faces of the cube must align with each other. The CSP can be solved efficiently in Haskell by employing monadic constraint solving, which also gives an elegant interface to employ different search strategies. In the future I hope to adapt this approach to all flavours of cubical type theory, to derive more involved arguments solving several mutually dependent goals at once, and to derive counterexamples to errant goals.
A highly experimental implementation of the solver can be found at https://github.com/maxdore/csolver. Eventual goal is to provide a tactic or internal implementation in Cubical Agda akin to Agsy.
15.00–15.20: Kenji Maillard (Inria Rennes  Bretagne Atlantique), The multiverse — Logical modularity for proof assistants
(J.w.w. Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau and Éric Tanter.)
Proof assistants play a dual role as programming languages and logical systems. As programming languages, proof assistants offer standard modularity mechanisms such as firstclass functions, type polymorphism and modules. As logical systems, however, modularity is lacking, and understandably so: incompatible reasoning principles — such as univalence and uniqueness of identity proofs — can indirectly lead to logical inconsistency when used in a given development, even when they appear to be confined to different modules. The lack of logical modularity in proof assistants also hinders the adoption of richer programming constructs, such as effects. In this talk, I will describe a general typetheoretic approach called the multiverse to endow proof assistants with logical modularity. The multiverse consists of multiple universe hierarchies that statically describe the reasoning principles and effects available to define a term at a given type. We identify sufficient conditions for this structuring to modularly ensure that incompatible principles do not interfere, and to locally restrict the power of dependent elimination when necessary. This extensible approach generalizes the adhoc treatment of the sort of propositions in the Coq proof assistant.
15.50–16.10: Iosif Petrakis (LudwigMaximiliansUniversität München), Positive negation in constructive mathematics •
In standard constructive logic negation is treated as in classical logic in a negativistic and weak way. This is in contrast to the use of a positive and strong “or” and “exists”. In constructive mathematics however, we often find a positive and strong approach to negatively defined concepts, like that of inequality. This fact motivates a clear distinction between a positive and strong negation and the standard weak negation. Bringing together older ideas of Griss and Nelson and recent work of Shulman and ours, we investigate the role of a positive and strong negation in Bishopstyle constructive mathematics.
16.10–16.30: Raffael Stenzel (Masaryk University), Higher geometric sheaf theories •
The theory of classifying toposes is a crucial feature of what makes the Elephant what it is: A powerful environment for varying mathematical expressions of related ideas to converge to a single concept. Particularly, it allows to manage the intricate world of continuously varying algebraic structures over topological spaces by way of the thoroughly organized syntax of symbolic logic.
As of yet, an according theory of classifying infinitytoposes has not been developed for various obstructive reasons. With this ultimate goal in mind, in this talk I propose a canonical sheaf theory for geometric infinitycategories; here, the notion of geometric infinitycategory generalizes Anel and Joyal’s definition of infinitylogoi in straightforward fashion. I do so by moving away from the classical sheaf condition over topological spaces — and over geometric categories more generally — and introduce a stronger limit preserving property instead. We will see that the according higher geometric sheaves differ from the ordinary ones only by a subtle cotopological fragment. Yet it turns out that this fragment is crucial in various aspects. As a case in point, I show that every infinitytopos is the theory of higher geometric sheaves over itself, and that the same is generally not true for the ordinary geometric sheaves over itself.
Concerning this workshop, I would be particularly interested in discussions on whether or not the associated higher covers are the right way to think about — and eventually obtain — a notion of geometric HoTT’s, in such a way that these higher geometric sheaf theories present classifying infinitytoposes for them.
16.30–17.30: Anja Petković Komel (TU Wien), The essence of elaboration •
When using type theories in proof assistants the full syntax can quickly become too verbose to handle. One common solution to this problem is to design two type theories: a fully annotated type theory which has good metatheoretic properties, is suitable for algorithmic processing and resides in the kernel of the proof assistant, and an economic one for the users’ input. The two theories are linked by elaboration, a reconstruction of missing information that happens during, or in parallel with, typechecking.
In this talk we will take a look at the typetheoretic account of an elaboration map: a section of a “forgetful” typetheoretic transformation $r : S \to T$ from the fully annotated type theory S, which we will call standard type theory, to the economic one T, called a finitary type theory. This definition of elaboration map enjoys two important metatheoretic properties: every finitary type theory has an elaboration map to a standard type theory and it satisfies a universal property, making it unique upto judgemental equality. We will also consider algorithmic aspects of elaboration and relate it to typechecking.
This is joint work with Andrej Bauer.
Saturday 21 May
10.00–11.00: András Kovács (Eötvös Loránd University), Typetheoretic signatures for algebraic theories and inductive types •
In the context of proof assistants, inductive types are specified by signatures of certain syntactic schemata. More generally, algebraic theories can be likewise specified by syntactic signatures. I present several type theories (“theories of signatures”) where certain closed types can be viewed as algebraic/inductive signatures. By varying available type formers, we can describe various classes of algebraic theories, ranging from singlesorted finite product theories to higher inductiveinductive theories. The type theories of signatures can be modeled in various categories of algebras; for instance, we can interpret a quotient inductive signature as an 1category of algebras, and a higher inductiveinductive signature as a higher category. Thus, theories of signatures can be viewed as very simple directed type theories, where variance issues are avoided by disallowing higherorder functions. I also describe term algebra constructions: this means constructing initial algebras from syntactic terms of theories of signatures. This can be used as an intermediate step in reducing large classes of inductive types to basic type formers.
11.20–12.20: Théo Winterhalter (Max Planck Institute for Security and Privacy (MPISP)), MetaCoq: Sound and complete type checking for Coq, in Coq •
Coq is built around a welldelimited kernel that performs type checking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in Coq is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in Coq.
With MetaCoq we offer both a formal specification of the metatheory of Coq (currently excluding ηlaws, modules, strict propositions and template polymorphism) and an implementation of a type checker that we prove correct and complete with respect to this specification. In order to do this, we have to prove several metatheoretic properties such as confluence of the reduction or subject reduction, and rely on the axiom of strong normalisation.
I will mostly focus on the type checker and the metatheory of Coq developed as part of the MetaCoq project lead by Matthieu Sozeau and including Jakob Botsch Nielsen, Simon Boulier, Yannick Forster, Meven LennonBertrand and Nicolas Tabareau.
14.00–15.00: Taichi Uemura (University of Stockholm), Normalization for initial spacevalued models of type theories •
Given a type theory, one can construct its initial setvalued model but also its initial spacevalued model. The coherence problem asks if the initial spacevalued model is actually setvalued. If this is the case, then the initial setvalued model admits a unique morphism to an arbitrary spacevalued model, which allows us to interpret the type theory in higher structures.
We develop a normalization technique for the initial spacevalued model to solve the coherence problem. Once we have proved that every type or term in the initial spacevalued model has a unique normal form, calculation of the path spaces of the initial spacevalued model is reduced to calculation of the path spaces between normal forms. The space of normal forms is defined as an (nonhigher) inductive type in a certain ∞topos, so its path spaces are easy to calculate.
Our normalization technique is a higherdimensional version of normalization by evaluation. This is possible thanks to Bocquet, Kaposi, and Sattler’s relative induction principle and Sterling’s synthetic Tait computability. The relative induction principle gives us a definition of the category of renamings suitable for ∞categorical generalization. The idea of synthetic Tait computability is to use extensional type theory as an internal language for glued 1topoi to construct logical predicates. Its higher analogue is to use homotopy type theory as an internal language for glued ∞topoi to construct logical predicates.
15.00–15.20: Jonas Frey (Carnegie Mellon University), Characterizing clanalgebraic categories •
Clans [2] provide a categorical notion of dependent algebraic theory that can be seen as syntaxfree abstraction of Cartmell’s generalized algebraic theories and as such is closely related to concepts like contextual categories and categories with families. Viewed as algebraic theories, clans are equally expressive as finitelimit theories but contain more information: the same finitelimit theory can have representations by different clans, and in particular different clans can have the same category of Setmodels. The additional information encoded in a clan T gives rise to a weak factorization system (E,F) on the locally finitely presentable category Mod(T) (first considered by Henry), from which the clan can be reconstructed up to Morita equivalence.
In this talk I will present a biequivalence between a 2category of clans, and a 2category of “clanalgebraic categories”: these are locally finitely presentable categories equipped with a weak factorization system satisfying an exactness condition. This characterization of clanalgebraic categories can be seen as a generalization of the characterization of algebraic categories as “exact cocomplete categories that are generated by perfectly presentable objects” given in [1].
 Adámek, Jiří, Jiří Rosický, and Enrico Maria Vitale. Algebraic theories: a categorical introduction to general algebra. Vol. 184. Cambridge University Press, 2010.
 Joyal, André. Notes on clans and tribes. arXiv preprint arXiv:1710.10238 (2017).
15.20–15.40: Jacopo Emmenegger, Bsystems and Csystems are equivalent •
Csystems were defined by Cartmell as models of generalized algebraic theories. Bsystems were defined by Voevodsky in his quest to formulate and prove an initiality theorem for type theories. I will speak about a joint work with Benedikt Ahrens, Paige Randall North and Egbert Rijke where we prove Voevodsky’s conjecture that the categories of Bsystems and of Csystems are equivalent. We do so by specialising a more general equivalence between nonstratified versions of Bsystems and Csystems, which we name Esystems and CEsystems, respectively.
16.00–16.20: Sergei Soloviev (IRIT, University of Toulouse), Consequences of Computational Asymmetry in VerifierFalsifier Games •
Orginally, Game Theoretic Semantics (GTS) was developed as a variant of verification procedure for already existing logical semantics. These semantics could be classical, constructive etc. I explore (or, rather, start the exploration) of how the GTS may be modified, or even “perversed”, if there are significant differences in the computational power of players. More recent works on GTS for type theories are viewed in this context.
References related to this talk:
 Thierry Coquand “A Semantics of Evidence for Classical Arithmetic” (1995)
 J.L. Krivine “Dependent choice, ‘quote’ and the clock” (2003)
 Denis Bonnay “Preuves et jeux sémantiques” (2004)
 Boyer and Sandu “Between Proof and Truth” (2012)
 Yamada “Game Semantics of MartinLöf Type Theory” (2013), Odintsov, Speranski
 Shevchenko “Hintikka’s IndependenceFriendly Logic Meets Nelson’s Realizability” (2018)
16.20–16.40: Henning Basold (Leiden University), Towards behavioural types as coalgebras •
Category theoretical approaches have been fruitful in the investigation of type theories and their syntax, but typically syntax is treated inductively via algebras. In this talk, I would like to discuss how session types and contextfree session types can be approached via coalgebras, which allows us to handle elegantly problems via coalgebraic techniques that purely syntactic approaches render more opaque. Using coalgebra to deal with the syntax of session types may lead the way to a coinductive treatment of general behavioural types and the corresponding logics.
16.40–17.40: Ivan Di Liberti (University of Stockholm), Bipresentable 2categories and (bilex) 2sketches
Motivated by the study of several 2categories of (first order) theories (Lex, Reg, Coh, Ex, Ext), we introduce bipresentable 2categories and show that those provide a solid framework to develop semantics for 2sketches, and in general describe 2categories of theories. We define biaccessible and bipresentable 2categories in terms of bicompact objects and bifiltered bicolimits. We prove a biaccessible right biadjoint functor theorem and deduce a 2dimensional GabrielUlmer duality relating small bilex 2categories and finitely bipresentable 2categories. Finally, we show that 2categories of pseudoalgebras of finitary 2monads on Cat are finitely bipresentable, which in particular captures the case of Lex, the 2category of small lex categories. Invoking the technology of lexcolimits, we prove further that several 2categories arising in categorical logic (Reg, Ex, Coh, Ext, Adh, Pretop) are also finitely bipresentable.