Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Dan Christensen <jdc@uwo.ca>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>,
	HoTT Electronic Seminar Talks
Subject: [HoTT] HoTTEST Event for Junior Researchers starts this week
Date: Mon, 3 Oct 2022 20:14:52 +0000	[thread overview]
Message-ID: <87k05gaclf.fsf@uwo.ca> (raw)
In-Reply-To: <87r12c0xdl.fsf@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


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
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

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.

      parent reply	other threads:[~2022-10-03 20:14 UTC|newest]

Thread overview: 3+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2022-07-23 13:30 [HoTT] HoTTEST Event for Junior Researchers, Fall 2022 Dan Christensen
2022-08-19  5:52 ` [HoTT] Last call: " Dan Christensen
2022-10-03 20:14 ` Dan Christensen [this message]

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=87k05gaclf.fsf@uwo.ca \
    --to=jdc@uwo.ca \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=hott-electronic-seminar-talks@googlegroups.com \


* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).