The Internet, July 5-7, 2020

Co-located with FSCD 2020, The Internet

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.

- Click here to register for HoTT/UF 2020.
- Click here for registration for the main conferences FSCD and IJCAR.

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

**Marco Benini and Roberta Bonacina**: A proof-theoretical semantics for homotopy type theory**Dan Christensen and Luis Scoccola**: The Hurewicz Theorem in Homotopy Type Theory**Nima Rasekh**: A Step towards Non-Presentable Models of Homotopy Type Theory**Taichi Uemura and Hoang Kim Nguyen**: ∞-type theories**Benedikt Ahrens, Nikolai Kudasov, Peter Lefanu Lumsdaine and Vladimir Voevodsky**: Categorical structures for type theory in univalent foundations, II**Marco Girardi, Roberto Zunino and Marco Benini**: A general syntax for nonrecursive Higher Inductive Types**Eric Faber and Benno van den Berg**: Effective Kan fibrations in Simplicial Sets**Andrei Rodin**: Computer-Assisted Proofs and Mathematical Understanding: the case of Univalent Foundations**Jacopo Emmenegger, Fabio Pasquali and Giuseppe Rosolini**: Elementary fibrations and (algebraic) weak factorisation systems**Maximilian Doré and Samson Abramsky**: Towards Simplicial Complexes in Homotopy Type Theory**Mark Bickford**: Cubical type theory with several universes in Nuprl**Gianluca Amato, Marco Maggesi, Maurizio Parton and Cosimo Perini Brogi**: Universal Algebra in UniMath**Tom de Jong**: Domain theory in predicative Univalent Foundations**Rafaël Bocquet**: Coherence of definitional equalities in type theory**Emil Holm Gjørup and Bas Spitters**: Congruence closure in Cubical Type Theory**Todd Waugh Ambridge**: Formalising the Escardó-Simpson Closed Interval Axiomatisation in Univalent Type Theory**Carlo Angiuli, Anders Mörtberg and Max Zeuner**: Representation Independence via the Cubical Structure Identity Principle**Håkon Robbestad Gylterud**: Non-wellfounded sets in HoTT**Andrew Swan**: Towards an enveloping infinity topos for the effective topos**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

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

- Benedikt Ahrens,
`B.Ahrens@cs.bham.ac.uk`

(University of Birmingham) - Chris Kapulkin,
`kkapulki@uwo.ca`

(Western University)