Abstract: In topology, results such as Brouwer's fixed point theorem are often not accessible from the homotopy-theoretic point of view, since they usually depend on more than just the homotopy type of a given space, and many are also not constructively provable. By working in the setting of homotopy type theory, we will see that studying the property "every self-map has a fixed point" provides a different, homotopy-invariant notion.

After constructing counterexamples, we show that classifying spaces of non-Abelian finite simple groups satisfy this property. Along the way, we compute the homotopy groups of the space of maps into a classifying space in homotopy type theory. In particular, if G and H are finite groups, we will show that we can completely describe the space of maps between their classifying spaces constructively. Our results are formalised in the Rocq proof assistant.

This talk is based on joint work with Dan Christensen.

Abstract: Dependent type theory is an alternative foundation to mathematics that has provided the basis for proof assistant software such as Rocq or Lean. This is enabled by the nice computational properties of type theory, but another valuable aspect of type theory is its syntax/semantics relationship with category theory. This relationship allows us to not just study our foundations using category theory, but also to study (higher) category theory using type theory. While we understand this relationship well in certain cases, such as with the lambda calculus and Cartesian closed categories, for many type theories, including most of those used in proof assistants, our understanding of this relationship is still incomplete. In this talk I will discuss the nature of this relationship and explain part of the internal language conjectures which posit an equivalence between certain type theories and higher categories.