[HoTT] HoTTEST Event for Junior Researchers starts this week

[Dan Christensen <jdc@uwo.ca>]

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.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/87k05gaclf.fsf%40uwo.ca.