Cubical methods in homotopy type theory and univalent foundations

Cubical methods have played an important role in the development of Homotopy Type Theory and Univalent Foundations (HoTT/UF) in recent years. The original motivation behind these developments was to give constructive meaning to Voevodsky’s univalence axiom, but they have since then led to a range of new results. Among the achievements of these methods is the design of new type theories and proof assistants with native support for notions from HoTT/UF, syntactic and semantic consistency results for HoTT/UF, as well as a variety of independence results and establishing that the univalence axiom does not increase the proof theoretic strength of type theory. This paper is based on lecture notes that were written for the 2019 Homotopy Type Theory Summer School at Carnegie Mellon University. The goal of these lectures was to give an introduction to cubical methods and provide sufficient background in order to make the current research in this very active area of HoTT/UF more accessible to newcomers. The focus of these notes is hence on both the syntactic and semantic aspects of these methods, in particular on cubical type theory and the various cubical set categories that give meaning to these theories.

Khovanov–Lipshitz–Sarkar homotopy type for links in thickened higher genus surfaces

We discuss links in thickened surfaces. We define the Khovanov–Lipshitz–Sarkar stable homotopy type and the Steenrod square for the homotopical Khovanov homology of links in thickened surfaces with genus [Formula: see text]. A surface means a closed oriented surface unless otherwise stated. Of course, a surface may or may not be the sphere. A thickened surface means a product manifold of a surface and the interval. A link in a thickened surface (respectively, a 3-manifold) means a submanifold of a thickened surface (respectively, a 3-manifold) which is diffeomorphic to a disjoint collection of circles. Our Khovanov–Lipshitz–Sarkar stable homotopy type and our Steenrod square of links in thickened surfaces with genus [Formula: see text] are stronger than the homotopical Khovanov homology of links in thickened surfaces with genus [Formula: see text]. It is the first meaningful Khovanov–Lipshitz–Sarkar stable homotopy type of links in 3-manifolds other than the 3-sphere. We point out that our theory has a different feature in the torus case.

Almost-extreme Khovanov spectra

We introduce a functor from the cube to the Burnside 2-category and prove that it is equivalent to the Khovanov spectrum given by Lipshitz and Sarkar in the almost-extreme quantum grading. We provide a decomposition of this functor into simplicial complexes. This decomposition allows us to compute the homotopy type of the almost-extreme Khovanov spectra of diagrams without alternating pairs.

Area-perimeter duality in polygon spaces

Two natural foliations, guided by area and perimeter, of the configurations spaces of planar polygons are considered and the topology of their leaves is investigated in some detail. In particular, the homology groups and the homotopy type of leaves are determined. The homology groups of the spaces of polygons with fixed area and perimeter are also determined. Besides, we extend the classical isoperimetric duality to all critical points. In conclusion a few general remarks on dual extremal problems in polygon spaces and beyond are given.

Synthetic topology in Homotopy Type Theory for probabilistic programming

The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, continuous distributions have to be discretized because the corresponding measures cannot be defined on all subsets of their carriers. This paper proposes the use of synthetic topology to model continuous distributions for probabilistic computations in type theory. We study the initial σ-frame and the corresponding induced topology on arbitrary sets. Based on these intrinsic topologies, we define valuations and lower integrals on sets and prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed.

The Cantor–Schröder–Bernstein Theorem for $$\infty $$-groupoids

We show that the Cantor–Schröder–Bernstein Theorem for homotopy types, or $$\infty $$ ∞ -groupoids, holds in the following form: For any two types, if each one is embedded into the other, then they are equivalent. The argument is developed in the language of homotopy type theory, or Voevodsky’s univalent foundations (HoTT/UF), and requires classical logic. It follows that the theorem holds in any boolean $$\infty $$ ∞ -topos.