| CARVIEW |
Select Language
HTTP/2 301
server: GitHub.com
content-type: text/html
location: https://hott-uf.github.io/2020/
access-control-allow-origin: *
strict-transport-security: max-age=31556952
expires: Mon, 29 Dec 2025 15:43:35 GMT
cache-control: max-age=600
x-proxy-cache: MISS
x-github-request-id: 1EFE:15317B:906571:A1FA36:69529F4E
accept-ranges: bytes
age: 0
date: Mon, 29 Dec 2025 15:33:35 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210082-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767022415.944381,VS0,VE207
vary: Accept-Encoding
x-fastly-request-id: c77041e2a3941613764877bd6be4d66139946f63
content-length: 162
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Tue, 11 Nov 2025 16:10:16 GMT
access-control-allow-origin: *
strict-transport-security: max-age=31556952
etag: W/"69135fe8-2fc4"
expires: Mon, 29 Dec 2025 15:43:35 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: 4619:2C10E1:90A6C0:A23C73:69529F4F
accept-ranges: bytes
age: 0
date: Mon, 29 Dec 2025 15:33:35 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210082-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767022415.181144,VS0,VE214
vary: Accept-Encoding
x-fastly-request-id: d643bd27c419347c9c03227c72c206ee997204fb
content-length: 4549
HoTT/UF 2020
Workshop on Homotopy Type Theory/ Univalent Foundations
The Internet, July 5-7, 2020
Co-located with FSCD 2020, The Internet
How to join the workshop
If you have registered in time, you will receive an email in the morning of Sunday, 5 July 2020, with a link to a Zoom meeting. If you have not received such a link, request it by sending an email to the organizers.Videos of the talks
Available on the HoTT/UF 2020 YouTube channel.Overview
Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory.
The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory/Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory.
Registration
Registration is free of charge, but mandatory.- Click here to register for HoTT/UF 2020.
- Click here for registration for the main conferences FSCD and IJCAR.
Invited speakers
- Carlo Angiuli (Carnegie Mellon University)
From raw terms to recollement
In this two-part talk, I will start with an overview of the standard syntactic metatheorems of type theory, the proof techniques we have historically used to establish these properties, and how these properties are leveraged by proof assistants. In the second part, I present joint work with Jonathan Sterling and Daniel Gratzer on a synthetic method of computability for proving canonicity and normalization purely in the internal language of a glued topos. In particular, the "syntactic" and "semantic" aspects of computability families are projected via complementary open and closed modalities.
Video of the talk (YouTube) - Liron Cohen (Ben-Gurion University)
Building Effectful Realizability Models, Uniformly
Constructive foundations have for decades been built upon realizability models for higher-order logic and type theory. These models, however, have a rather limited notion of realizability that only supports non-termination while avoiding many other effects that can (and should) be considered. In this talk we will present several extensions to the standard realizability models, incorporating non-deterministic and stateful computations, and explore their impact on the resulting theories. Furthermore, we will introduce a new model-theoretic tool for building such effectful realizability models uniformly.
Video of the talk (YouTube) - Pierre-Louis Curien (Université de Paris)
A syntactic approach to opetopes, opetopic sets and opetopic categories
Opetopes are shapes that were introduced by Baez and Dolan for an approach to a definition of higher categories. They can be concisely defined in the language of polynomial monads as trees whose nodes are themselves trees whose nodes etc. But opetopes are difficult combinatorial objects. I shall discuss one approach to a careful description of opetopes and, on the top of it, of two variants of opetopic sets, based on two different categories of opetopes, in which degeneracies are embodied in the objects (resp. in the morphisms). I’ll touch briefly and tentatively on the (tricky) axiomatics for higher categories via universality suggested by Eric Finster. The talk will reflect my own take on this subject, but will rely very much on joint work or continued conversations with Eric Finster, Amar Hadzihasanović, Cédric Ho Thanh and Samuel Mimram.
Video of the talk (YouTube)
Contributed talks
- Marco Benini and Roberta Bonacina: A proof-theoretical semantics for homotopy type theory
Video of the talk (YouTube) - Dan Christensen and Luis Scoccola: The Hurewicz Theorem in Homotopy Type Theory
Video of the talk (YouTube) - Nima Rasekh: A Step towards Non-Presentable Models of Homotopy Type Theory
Video of the talk (YouTube) - Taichi Uemura and Hoang Kim Nguyen: ∞-type theories
Video of the talk (YouTube) - Benedikt Ahrens, Nikolai Kudasov, Peter Lefanu Lumsdaine and Vladimir Voevodsky: Categorical structures for type theory in univalent foundations, II
Video of the talk (YouTube) - Marco Girardi, Roberto Zunino and Marco Benini: A general syntax for nonrecursive Higher Inductive Types
Video of the talk (YouTube) - Eric Faber and Benno van den Berg: Effective Kan fibrations in Simplicial Sets
Video of the talk (YouTube) - Andrei Rodin: Computer-Assisted Proofs and Mathematical Understanding: the case of Univalent Foundations
Video of the talk (YouTube) - Jacopo Emmenegger, Fabio Pasquali and Giuseppe Rosolini: Elementary fibrations and (algebraic) weak factorisation systems
Video of the talk (YouTube) - Maximilian Doré and Samson Abramsky: Towards Simplicial Complexes in Homotopy Type Theory
Video of the talk (YouTube) - Mark Bickford: Cubical type theory with several universes in Nuprl
Video of the talk (YouTube) - Gianluca Amato, Marco Maggesi, Maurizio Parton and Cosimo Perini Brogi: Universal Algebra in UniMath
Video of the talk (YouTube) - Tom de Jong: Domain theory in predicative Univalent Foundations
Video of the talk (YouTube) - Rafaël Bocquet: Coherence of definitional equalities in type theory
Video of the talk (YouTube) - Emil Holm Gjørup and Bas Spitters: Congruence closure in Cubical Type Theory
Video of the talk (YouTube) - Todd Waugh Ambridge: Formalising the Escardó-Simpson Closed Interval Axiomatisation in Univalent Type Theory
Video of the talk (YouTube) - Carlo Angiuli, Anders Mörtberg and Max Zeuner: Representation Independence via the Cubical Structure Identity Principle
Video of the talk (YouTube) - Håkon Robbestad Gylterud: Non-wellfounded sets in HoTT
Video of the talk (YouTube) - Andrew Swan: Towards an enveloping infinity topos for the effective topos
Video of the talk (YouTube) - Jonas Frey: A refinement of Gabriel-Ulmer duality
Slides of the talk (pdf) - Hugo Herbelin and Hugo Moeneclaey: Investigations into syntactic iterated parametricity and cubical type theory
Video of the talk (YouTube)
Program
Program committee
- Benedikt Ahrens (University of Birmingham)
- Paolo Capriotti (Technische Universität Darmstadt)
- Chris Kapulkin (University of Western Ontario)
- Nicolai Kraus (University of Birmingham)
- Peter LeFanu Lumsdaine (Stockholm University)
- Anders Mörtberg (Stockholm University)
- Paige Randall North (Ohio State University)
- Nicolas Tabareau (Inria Nantes)
Organizers
- Benedikt Ahrens,
B.Ahrens@cs.bham.ac.uk(University of Birmingham) - Chris Kapulkin,
kkapulki@uwo.ca(Western University)