HoTTEST Event for Junior Researchers, Fall 2022

[Dan Christensen]

Call for speakers:

HoTTEST Event for Young Researchers
October to December, 2022 (precise dates will be announced later)
11am to 1pm Eastern, followed by an informal gathering

Deadline: August 26, 2022 (anywhere on earth)

Request to speak: https://forms.gle/oKDj3SPDWmeSe9ut6

In Fall 2022, the HoTTEST seminar will host Zoom talks by junior
researchers in homotopy type theory, with priority given to those who
are on the academic job market. The talks will most likely be 30
minutes long, and we plan to also hold an informal discussion session
after each day's talks.

If you are interested in giving a talk, please use the link above
to submit your request.

We will also have other talks during the fall and winter, with
speakers to be announced. For more about the HoTTEST seminar, see:

https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

Organizers:

Carlo Angiuli
Dan Christensen
Chris Kapulkin
Emily Riehl

[Dan Christensen]

Reminder: the deadline for applications is one week from today.
Please fill out the form at the link below if you wish to speak.

-----

[Dan Christensen]

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

https://groups.google.com/forum/#!forum/hott-electronic-seminar-talks

for future updates. Further information, including videos and slides
from past talks, is at:

http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html

Dan

(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen,
Chris Kapulkin, and Emily Riehl.)

---

October 6 11:30 Eastern
Amélia Liao
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
perspective.

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
Chris Grossack
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.