Stefania Damato, The groupoid CwF of containers

Axel Ljungström, A formalisation of the Serre finiteness theorem

Greg Langmead, Discrete differential geometry in homotopy type theory

Jon Sterling, Is it time for a new proof assistant?

Mitchell Riley, Tiny types and cubical type theory

Jonathan Weinberger, Directed univalence and the Yoneda embedding for synthetic ∞-categories

Martín Hötzel Escardó, Injective types

Mario Carneiro, Lean4Lean: Towards a Verified Typechecker for Lean, in Lean

Paige North, Coinductive control of inductive data types

Niels van der Weide, The internal languages of univalent categories

Tashi Walde, An axiomatization of synthetic category theory

Max Zeuner, Univalent foundations of constructive algebraic geometry

Floris van Doorn, Formalizing a proof of Carleson's theorem

Reid Barton, Directed aspects of condensed type theory

Andreas Nuyts, Higher pro-arrows: Towards a model for naturality pretype theory

Dan Christensen, Sphere bundles and their invariants

Evan Cavallo, Why some cubical models don't present spaces

Greta Coraglia, On the fibration of algebras

Rafaël Bocquet, Strict Rezk completions of models of HoTT and homotopy canonicity

Émile Oleon, Delooping cyclic groups with lens spaces in homotopy type theory

Urs Schreiber, Topological quantum programming via linear homotopy types

David Jaz Myers, The tangent bundles of spheres

Ingo Blechschmidt, Towards multiversal modal operators for homotopy type theory

David Wärn, Path spaces of pushouts via a zigzag construction

Elisabeth Stenholm, Non-wellfounded sets in homotopy type theory

Felix Cherubini, A foundation for synthetic algebraic geometry

Nikolai Kudasov, Rzk proof assistant and simplicial HoTT formalization

Maria Emilia Maietti, A comparison between the Minimalist Foundation and Homotopy Type Theory

Omar Antolín Camarena, HoTT lessons for algebraic topologists

Daniel Gratzer, Modalities and (weak) dependent right adjoints

Hoang Kim Nguyen, Directed univalence in simplicial sets

Loïc Pujet, Observational Type Theory meets CIC

Andrew Swan, Double negation stable h-propositions in cubical sets

Johan Commelin, The Liquid Tensor Experiment

Philipp Joram, Final Coalgebras of Analytic Functors in Homotopy Type Theory

Astra Kolomatskaia, Semi-simplicial types

Jacob Neumann, (Co)ends and (Co)structure

Jarl G. Taxerås Flaten, Central H-spaces and banded types

Tom de Jong, Acyclic types and epimorphisms in HoTT

Colin Zwanziger, Hofmann-Streicher universes via coalgebra

Evan Cavallo, Cubes with one connection and relative elegance

Max Zeuner, A univalent formalization of affine schemes

Axel Ljungström, Calculating a Brunerie number

Chris Grossack, Where are the open sets? Comparing HoTT with Classical Topology

Amélia Liao, Univalent Category Theory

Chaitanya Leena Subramaniam, Semantics of HoTT

Favonia, Cartesian cubical type theory

Jonas Frey, Introduction to modalities

Pierre Cagne, Group theory without groups

Jon Sterling, How to code your own type theory

HoTT Problem Session 12: Univalent combinatorics (Tom) -- HoTTEST Summer School 2022

HoTT Problem Session 12: Univalent combinatorics (Artem) -- HoTTEST Summer School 2022

HoTT Lecture 12: Univalent combinatorics -- HoTTEST Summer School 2022

Agda Problem Session 9: Homogeneous comp. & cubical univalence (Astra) -- HoTTEST Summer School 2022

Agda Problem Session 9: Homogeneous comp. & cubical univalence (Axel) -- HoTTEST Summer School 2022

Agda Lecture 9: Homogeneous composition and cubical univalence -- HoTTEST Summer School 2022

HoTT Problem Session 11: The univalence axiom (Jacob) -- HoTTEST Summer School 2022

HoTT Lecture 11: The univalence axiom -- HoTTEST Summer School 2022

HoTT Problem Session 11: The univalence axiom (Jarl) -- HoTTEST Summer School 2022

Agda Problem Session 8: Quotients and Higher Inductive Types (Astra) -- HoTTEST Summer School 2022