ABSTRACT. Type theory is a formal system widely used in most modern proof assistants. The language of type is convenient and powerful, and closely matches the way mathematicians express themselves conceptually. There are, however, some phenomena in type theory that some mathematicians are uneasy about. In particular, the identity type has intricacies that many mathematicians rather squash out by assuming axiom K, which asserts that equality is always a proposition. There is, however, much to learn about type theory if we resist our temptation to assume this axiom.

Types naturally come with the structure of a higher groupoid, where the identifications are the 1-cells, the identifications between identifications are 2-cells, and so on. By this observation we can also say that a pointed connected type is a higher group. More precisely, it is the classifying type of a higher group. Indeed, identifications can be concatenated, inverted, there is a unit identification called reflexivity, and these satisfy the laws of a higher group. Here we take the point of view that a higher group should be the space of symmetries of some object. In a pointed connected type, the object of which we consider the symmetries is the base point and the symmetries of that object are its self-identifications. This is an important observation: symmetries are identifications of an object with itself, and pointed connected types are concrete manifestations of (higher) groups as spaces of symmetry.

From this point of view we can develop all of group theory and higher group theory. A group action is simply a type family over the classifying type of the group. Group homomorphisms are simply pointed maps, and so on. In my lecture I will showcase how to interpret some of the most important concepts of group theory, with concrete examples.

ABSTRACT. University course topics such as logic, formal semantics, type theory, algorithms and data structures, all have mathematical prerequisites. CS students often struggle when presented with exercises that require mathematical rigour. Research, as well as personal experience, suggests that the approaches to teaching CS students are confident with differ from those for math students (analogous results have also been found within physics). CS students have usually been exposed to several programming courses before a class dedicated to theoretical computer science, where they have perhaps developed a confidentiality with a trial-and-error approach. On this basis, we hypothesise, that CS students will more easily learn the skills required for these courses, if they are supported by a tool that helps them exercise their mathematical rigorousness, while giving them a flavour of trial-and-error. However, as is tradition in CS education, through careful tool design, we would also like to encourage reflection, instead of exclusively solving problems by trial-and-error. From introduction to programming, we know that students like the ease of block-based frameworks (like Scratch), but students finds them less authentic.

ABSTRACT. The Linux kernel contains a subsystem called eBPF that allows safe execution of untrusted user-defined functions given as an assembly-level byte-code inside the kernel. Before the eBPF functions run they are analysed using static analysis by the in-kernel verifier. The verifier guards the integrity of the kernel by disallowing erroneous or malicious behaviour such as out-of-bounds memory access and non-termination. Thus, the verifier is not complete (but is hopefully sound). Termination is ensured by disallowing all back jumps (including recursion), thus eliminating all loops and recursion. Instead the kernel provide access to a so-called helper function named `bpf_loop`, which can best be described as a higher-order function for performing loops with an upper bound.

The verifier is only informally described, and in some cases details are only given in a implementation-near manner or not at all. Thus it is hard to know which rules you have to obey as a programmer; the situation is even worse if you are writing a code-generator for eBPF. Gershuni et al. presents an alternative formulation and implementation of an eBPF verifier. They describe that their analysis can handle loops.

We show how a type-system based on weakest pre-conditions can be used to faithfully model the in-kernel verifier. Post-conditions/abstract interpretation together with SMT solving enables automatic inference, while still permitting manual proofs when it falls short.

ABSTRACT. We discuss the problem of constructively defining an exponentiation function for the ordinals of the HoTT book, and prove its expected properties. We show that a fully general exponentiation function is definable if and only if excluded middle holds, but for ordinals of the form 1 + X we can define exponentiation (1 + X)^Y for arbitrary ordinals Y which satisfies the expected specification of exponentiation.

ABSTRACT. We show how types of finite sets and multisets can be constructed in ordinary dependent type theory, without the need for quotient types or working with setoids, and prove that these constructions realise finite sets and multisets as free idempotent commutative monoids and free commutative monoids, respectively. Both constructions arise as generalisations of C. Coquand’s data type of fresh lists, and we show how many other free structures also can be realised by other instantiations. All of our results have been formalised in Agda.

ABSTRACT. Quotient containers are set-valued containers with a selection of permissible isomorphisms of positions. They are interpreted as endofunctors on sets where labellings are identified according to those isomorphisms. More recently, symmetric containers were introduced to model types with symmetries. These are interpreted as endofunctors on groupoids. We investigate the relationship between the two notions. To any quotient container, we associate a symmetric container by delooping automorphism groups of positions. In the other direction, obtaining a quotient container is difficult constructively: it suffices to divide each groupoid of shapes into its pointed connected components, which should be implied by a variant of the axiom of choice. In any case we can deduce that a quotient container and its associated symmetric container have equivalent interpretations as set-endofunctors when truncated appropriately.

ABSTRACT. The relationship between structural and material set theory is well studied. Homotopy type theory/Univalent Foundations (HoTT/UF) can be seen as an extension of structural set theory to higher homotopy levels. This talk is part of an effort to investigate what the corresponding extension of set theory to higher homotopy levels could look like.

ABSTRACT. Formalization of mathematics is often seen as a way to formally verify mathematical definitions and theorems and gain more confidence in their veracity. However, in certain mathematical contexts and appropriately chosen type theories, pursuing formalization can result in additional advantages that can broaden our mathematical perspective. In this talk we will focus on the particular case of the Univalence Maxim and its application to the study and formalization of double category theory.

ABSTRACT. We propose a variation of the axiomatization of Zariski (higher) topos in synthetic algebraic geometry to an axiomatization of (separable) Stone spaces, with Stone duality, within a univalent homotopy type theory. This satisfies LLPO, and is reminiscent of the notion of light condensed sets. This can also be seen as a refinement of the work by Escardo and Xu on uniform continuity in Cantor space.

ABSTRACT. Various kinds of structured categories are used throughout mathematics and computer science. Internal to homotopy type theory, and assuming univalence, these structured categories are required to be invariant under some notion of sameness. In particular, categories are supposed to be invariant under (weak) equivalence. Those categories are said to be univalent. Furthermore, Ahrens, et. al. construct a completion operator, which constructs a free univalent category, from a (not-necessarily univalent) category. The completion operator is referred to as the Rezk completion. The theory of univalent categories, and the Rezk completion, has been shown to have analogous results for enriched categories, monoidal categories, etc. In this work in progress, we construct a (2-categorical) framework generalizing these results; in particular, the construction of the Rezk completion.

ABSTRACT. Type theory and category theory are deeply connected. This connection is exhibited by various theorems classifying the internal language of some kind of structured category as a suitable type theory. For example, the simply typed lambda calculus is the language of Cartesian closed categories, and Martin-Löf type theory is the language of locally Cartesian closed categories. Such theorems allow us to use type theory to reason about the objects and morphisms of a category.

However, in univalent foundations, several subtleties come up when we try to find a suitable internal language for classes of univalent categories. Often models of type theory, such as categories with families, assume a certain amount of strictness on the types. Technically, they require that the types form a set. However, since sets in univalent foundations do not satisfy this requirement, we do not have the usual CwFs of sets and of presheaves, and, more generally, it is not so that every category with finite limits gives rise to a CwF with suitable type formers. As a consequence, if one defines the syntax of type theory as a quotient inductive-inductive type, then one does not have a model given by sets without assuming UIP. Note that one could also use iterative sets, but the category of iterative sets is not univalent.

In this abstract, we study the internal language of univalent categories. More specifically, we construct an equivalence between univalent categories with finite limits and type theories with suitable type formers (unit types, product types, extensional identity types, and sigma types). This gives an analogue of Theorem 6.1 in the paper by Clairambault and Dybjer for univalent categories. Our results are formalized using the UniMath library in Coq.

ABSTRACT. Simplicial type theory was introduced by (Riehl--Shulman 2017) synthetic account of $\infty$-categories. Here, by ``$\infty$-categories'' we mean $(\infty,1)$-categories.

To begin with, the $\infty$-category of $\infty$-categories may be realized as a reflective subcategory of the category of simplicial spaces (Rezk 2001). Riehl--Shulman then observe that simplicial spaces---as an $\infty$-topos---support a model of homotopy type theory (HoTT). They further observe that by extending HoTT with a few key operations and axioms from this model, homotopy type theory may be transformed into a tool for reasoning directly about $\infty$-categories.

STT is already enough to prove a number of results, but it lacks well-adapted universes of $\infty$-categories. We combine simplicial type theory with a variant of multimodal type theory (MTT) (Gratzer 2020) to obtain a new type theory, called triangulated type theory. This enables us to construct a well-behaved universe Spaces of synthetic $\infty$-groupoids internally.

ABSTRACT. Universe types in Martin-Löf type theory (MLTT) have been investigated and utilised in various ways. In particular, universe types in a system of MLTT with W-types are often treated as type-theoretic counterparts of large cardinals or sets. Rathjen, Griffor and Palmgren introduced an extension MLQ of MLTT with two large universes and showed that an extension of Aczel's constructive set theory with inaccessible sets of all transfinite orders is interpretable in MLQ. The universe construction in MLQ was generalised by Palmgren: he introduced a family of systems of higher-order universe operators and verified that MLQ is an instance of these systems. Yet another universe type corresponding to large sets is the Mahlo universe type introduced by Setzer. A framework to unify these large universes has been already provided by Dybjer-Setzer's theory of indexed induction-recursion, except that this theory has defined a proof-theoretically weak variant of the Mahlo universe type. However, as is well known, the proof assistant Agda supports indexed induction-recursion as well, so one can still ask how the large universes above can be defined in Agda. We aim to formulate MLQ, the systems of higher-order universe operators, and the external Mahlo universe type by using Agda's indexed induction-recursion.

ABSTRACT. The imax-successor algebra, where imax is the function defined by imax(n, 0) = 0 and imax(n, s(m)) = max(n, s(m)), is used to represent universe levels in impredicative type theory, in particular with universe polymorphism which introduces level variables, so it is present in proof systems such as Coq and Lean. In particular, we need to know when two elements of this algebra are equivalent, and we may also want to decide the inequality. In this article, we introduce a canonical form for the terms of this algebra, and we provide a canonization algorithm. It permits deciding level equivalence by checking the canonical form equality, and also permits easily checking if a level is smaller than another one.

ABSTRACT. We provide a constructive, predicative justification of Setzer's Mahlo universe in type theory. Our approach is closely related to Kahle and Setzer's construction of an extended predicative Mahlo universe in Feferman's Explicit Mathematics. However, we work directly in Martin-Löf type theory extended with a Mahlo universe and obtain informal meaning explanations which extend (and slightly modify) those in Martin-Löf's article Constructive Mathematics and Computer Programming. We also present mathematical models in set-theoretic metalanguage and explain their relevance to the informal meaning explanations.