Fredrik Bakke & Egbert Rijke
Fredrik Bakke: The Yoneda lemma and complete Segal spaces in Homotopy Type Theory
Abstract: We'll wrap up the story from last time by proving the Yoneda lemma for Segal types and seeing how it generalizes identity induction, then we'll discuss univalence.
Egbert Rijke: Concrete univalent mathematics
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.
