The HoTTEST event for Junior Researchers begins this week, on Thursday,
October 6 at 11:30am Eastern. Each day will have two 30-minute talks,
followed by a discussion in Gather Town. The first two titles and
abstracts are below.
The Zoom link is https://zoom.us/j/994874377
Please subscribe to our mailing list at
for future updates. Further information, including videos and slides
from past talks, is at:
(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen,
Chris Kapulkin, and Emily Riehl.)
October 6 11:30 Eastern
Univalent Category Theory
Category theory is the study of structure across mathematics. Being a
mathematical subject itself, category theory should also encompass the
study of its own structural aspects.
A promising approach (Gray 1974; Di Liberti & Loregian 2019) is formal
category theory: studying the properties of the bicategory of categories
which make it possible to study category theory from a structural
A different idea is to approach categories as groupoids with extra
structure, something which finds itself naturally at home in HoTT, where
"groupoids" are particular types. This approach lends itself
particularly well to formalization in a proof assistant.
In the context of Cubical Agda, we recap the basic theory of univalent
categories (Ahrens, Kapulkin & Shulman 2013) and the move towards higher
univalent category theory (Capriotti & Kraus 2017; Ahrens et all 2019),
particularly the application of cubical syntax to fibred categories
(following Sterling & Angiuli 2021; Ahrens & Lumsdaine 2017).
October 6 12 Eastern
Where are the open sets? Comparing HoTT with Classical Topology
It's often said that Homotopy Type Theory is a synthetic description of
homotopy theory, but how do we know that the theorems we prove in HoTT
are true for mathematicians working classically? In this expository talk
we will outline the relationship between HoTT and classical homotopy
theory by first using the simplicial set semantics and then transporting
along a certain equivalence between (the homotopy categories of)
simplicial sets and topological spaces. We will assume no background
besides some basic knowledge of HoTT and classical topology.