Carlo Angiuli and Anders Mörtberg — Univalent Mathematics: Theory and Implementation

Homotopy Type Theory/Univalent Foundations (HoTT/UF) is a new foundation for mathematics based on novel connections between dependent type theory and homotopy theory. Recently, researchers have developed several reformulations of HoTT/UF that may be better suited for implementation in proof assistants, as well as extensions that natively account for mathematical structures such as spectra and higher categories. In this introductory talk for the session, we summarize the state of the art in proof assistants for HoTT/UF and related type theories.

Jesper Cockx — Rewriting Type Theory

Dependently typed languages such as Coq and Agda can statically guarantee the correctness of our proofs and programs. To provide this guarantee, they restrict users to certain schemes – such as strictly positive datatypes, complete case analysis, and well-founded induction – that are known to be safe. However, these restrictions limit the expressivity of the language and can make programs and proofs hard to write. In this talk I present Rewriting Type Theory (RTT), a dependently typed language with user-defined higher-order rewrite rules. These rewrite rules can be used to ease reasoning about existing definitions, and to extend the language with new constructs such as quotient types and exceptions. To ensure subject reduction in the presence of rewrite rules, I present a general method to check confluence based on Tait and Martin-Löf's triangle property of parallel reduction. I have implemented rewrite rules as an extension to Agda, and a formalization of the metatheoretic properties of RTT using MetaCoq is currently work in progress.

Kuen-Bang Hou (Favonia) — Nullable Compositions

Cubical type theory has come a long way to have univalent universes, higher inductive types, computational semantics, and Quillen equivalence to the standard homotopy theory. For it to be a foundation of practical tools, however, we still need more efficient normalization, type-checking, unification, and so on. One hot spot is compositions, the new gadget introduced in cubical type theory to impose proper higher-dimensional structure (fibrancy) in types. As an effort to eliminate compositions as much as possible, we have been considering variants of cubical type theory where there are no irreducible compositions at the zeroth dimension. I call these undesirable compositions as null compositions. To remove them, we have to kill all nullable compositions. We have found ways to implement this move in various cubical type theories, but a general solution is still lacking. This talk is an overview of what is currently known.

Daniel Gratzer — Multimodal Dependent Type Theory

We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, parametric quantification, and axiomatic cohesion. We reproduce examples from prior work in guarded recursion and axiomatic cohesion --- demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations. (Joint work with Alex Kavvos, Andreas Nuyts, and Lars Birkedal)

Valery Isaev — Arend proof assistant

I will discuss Arend, a proof assistant developed at JetBrains Research. The aim of Arend is to provide a powerful system for formalization results in homotopy type theory and in ordinary mathematics. To achieve the latter goal, we prove a flexible class system with subtyping, universe polymorphism with a powerful level inference mechanism, quotient sets with a convenient pattern matching principles for them. We also recently implemented a tactic framework which can be used to automate routine proofs and implement various EDSLs. Homotopic features of Arend include built-in universes of finite homotopy level, higher inductive types, univalence, and path types in the style of cubical type theories. I will talk about these features and also about our plans to implement language extensions that can be used to simplify reasoning about various higher structures.

Anja Petković — Andromeda 2 - your type theory à la carte

Andromeda 2 is a proof assistant that supports user-definable type theories by providing a metalanguage to operate with rules, judgements and derivations. The framework enables the user to work with various type theories, such as variants of Martin-Löf type theory, extensional type theory, and homotopy type theory. To make Andromeda 2 usable we have recently designed and implemented an extensible equality checking algorithm that supports user-defined computation rules (β-rules) and extensionality rules (inter-derivable with η-rules). In this talk I will present the basic features of Andromeda 2 and illustrate how to use them on some standard examples. This is joint work with Andrej Bauer and Philipp G. Haselwarter.

Loïc Pujet — Cubical Coq using Intensional Presheaves

Cubical type theory provides a computational interpretation of the univalence principle, based on cubical presheaf semantics. The cubical presheaf model is usually formulated inside an extensional meta-theory, but using an alternative definition of presheaves that behaves well in intensional type theory, Pédrot formulated the cubical presheaf model as a translation from type theory to itself. We make use of this translation to enrich intensional type theory with the Orton and Pitts axioms for cubical type theory, giving them a computational meaning in the presheaf model. As everything is done constructively, this preserves the good computational properties of intensional type theory: every integer derived using the axioms will compute to an actual integer after translation. This is a first step towards making cubical type theory compute inside Coq, resulting in a new modular framework for consistency and canonicity proofs of cubical type theories.

Mitchell Riley — A Type Theory for Parameterised Spectra

In synthetic homotopy theory, homology and cohomology theories are defined via the spectra that represent them. This works well for simple examples, but manipulating spectra defined internally in type theory quickly becomes cumbersome. In this talk we describe an extension of HoTT with axiomatic 'smash' and 'hom' types, with the intent of making 'stable synthetic homotopy theory' more tractable. Dependent types and linear types are combined in a novel way, presenting an interesting challenge for proof assistants.

Andrea Vezzosi — Indexed Families in Cubical Agda

Cubical Agda provides a proof assistant where Higher Inductive Types and Voevodsky's univalence principle have a computational interpretation. A distinguishing feature of Agda is dependent pattern matching for Indexed Inductive Families, which frees the user from having to explicitly deal with equalities of indexes. In Cubical Agda, however, transport for indexed families introduces new canonical forms that are not handled by how pattern matching definitions compute. We will see how to extend the elaboration of pattern matching clauses to account for these new canonical forms.

Matthew Weaver — A constructive model of directed univalence in bicubical sets

Directed type theory is an analogue of homotopy type theory where types represent categories, generalizing groupoids. A bisimplicial approach to directed type theory, developed by Riehl and Shulman, is based on equipping each type with both a notion of path and a separate notion of directed morphism. In this setting, a directed analogue of the univalence axiom asserts that there is a universe of covariant discrete fibrations whose directed morphisms correspond to functions—a higher-categorical analogue of the category of sets and functions. In this work, we give a constructive model of a directed type theory with directed univalence in bicubical, rather than bisimplicial, sets. We formalize much of this model using Agda as the internal language of a 1-topos, following Orton and Pitts. First, building on the cubical techniques used to give computational models of homotopy type theory, we show that there is a universe of covariant discrete fibrations, with a partial directed univalence principle asserting that functions are a retract of morphisms in this universe. To complete this retraction into an equivalence, we refine the universe of covariant fibrations using the constructive sheaf models by Coquand and Ruch. In this talk, I’ll present our constructive model of directed univalence, and discuss our ongoing efforts to implement a proof-assistant based on this type theory. (Joint work with Dan Licata)

Submission Guidelines

If you would like to give a talk in this ICMS session, you must first submit a proposed title and short abstract to the session organisers by email (anders.mortberg@math.su.se and cangiuli@cs.cmu.edu).

Speakers at this session may also optionally submit an extended abstract (4-8 pages) through the ICMS EasyChair page. Accepted extended abstracts will appear in an issue of Springer's Lecture Notes in Computer Science (LNCS). See this conference webpage for more details.

Deadlines

• Short Abstract Submission: 23 Feb

• Extended Abstract Submission: 27 March

• Software Demo Submission: 30 March

• PC decision on extended abstracts: 27 April

• Camera ready papers: 9 May