Monday	Tuesday	Wednesday	Thursday
8:30 - 9:00	Coffee and registration	Coffee	Coffee	Coffee
9:00 - 10:00	CoquandA type theoretic model of synthetic algebraic geometry	BergnerDiscreteness and completeness conditions for (∞,n)-categories	KovácsEfficient Evaluation for Cubical Type Theories	MörtbergComputational Synthetic Homotopy Theory
10:00 - 10:30	HutzlerA Foundation for Synthetic Algebraic Geometry	AnelDependent type theories and base change theorems	RoseDeciding the cofibration logic of cartesian cubical type theories	De JongOn epimorphisms and acyclic types in HoTT
10:30 - 11:00	Coffee	Coffee	Coffee	Coffee
11:00 - 11:30	CherubiniČech Cohomology in Homotopy Type Theory	Ljungström*Symmetric Monoidal Smash Products in HoTT	UskupluCofibrancy of The Exo-type of Natural Numbers	ChristensenExt groups in homotopy type theory
11:30 - 12:00	MyersOrbifolds in Synthetic Differential Cohesive HoTT	MartiniInternal higher topos theory	YukselOn the logic of sets in the simplicial model	FlatenCentral H-spaces and banded types
12:00 - 12:30	RileyCommuting Cohesions	FreyDuality for Clans and the Fat Small Object Argument	SpadettoPropositional dependent type theories: a conservativity result for homotopy elementary types	LavenirHilton-Milnor's theorem in higher categories
12:30 - 14:00	Lunch	Lunch	Lunch	Lunch
14:00 - 14:30	AwodeyAlgebraic type theory	WeinbergerInternal sums for synthetic fibered (∞,1)-categories	DamatoSpecifying QIITs using Containers	WeaverTheory and Implementation of Bicubical Directed Type Theory
14:30 - 15:00	Leena SubramaniamThe FOLDS theory associated to a contextual category	CherradiFinite colimits in an elementary higher topos	NeumannPresheaf Models of Polarized Higher-Order Abstract Syntax	DeanDirected Types are Weak ω-Categories
15:00 - 15:30	CioffoBiased elementary doctrines and quotient completions	HartColimits in the category of pointed types	RijkeThe agda-unimath library	AlliouxOpetopic Methods in Homotopy Type Theory
15:30 - 16:00	Coffee	Coffee	Coffee	Coffee
16:00 - 16:30	SwanOracle modalities	GratzerControlling unfolding in type theory using extension types	Shulman†The unifying power of modal type theory	Jackπ₄𝕊³ ≇ 1 and another Brunerie number in CCHM
16:30 - 17:00	SpeightGroupoidal Realizability Over an Untyped Cubical Lambda-Calculus	BerryFormalization Computation: Categorical Normalization by Evaluation		BakerEckmann-Hilton and the Hopf Fibration in Homotopy Type Theory
17:00 - 17:30	De JongRelating ordinals in set theory to ordinals in type theory			HerzogGoursat Homology
17:30 - 18:00			Reception
18:00 -	BBQ

• ^† Vladimir Voevodsky Memorial Lecture
• ^* Recipient of Best Student Paper Award
• Special session in honor of André Joyal’s contributions to HoTT on his 80th birthday

Invited talks

• Julie Bergner, Discreteness and completeness conditions for (∞,n)-categories
• Thierry Coquand, A type theoretic model of synthetic algebraic geometry [slides]
• András Kovács, Efficient Evaluation for Cubical Type Theories [slides]
• Anders Mörtberg, Computational Synthetic Homotopy Theory [slides]

Vladimir Voevodsky memorial lecture

• Michael Shulman, The unifying power of modal type theory [slides]

Contributed talks

• Antoine Allioux, Opetopic Methods in Homotopy Type Theory [slides]
• Mathieu Anel and Jonathan Weinberger, Dependent type theories and base change theorems [slides]
• Steve Awodey, Algebraic type theory [slides]
• Raymond Baker, Eckmann-Hilton and the Hopf Fibration in Homotopy Type Theory [slides]
• David Berry and Marcelo Fiore, Formalization Computation: Categorical Normalization by Evaluation [slides]
• El Mehdi Cherradi and Nima Rasekh, Finite colimits in an elementary higher topos [slides]
• Ingo Blechschmidt, Felix Cherubini and David Wärn, Čech Cohomology in Homotopy Type Theory [slides]
• J. Daniel Christensen and Jarl G. Taxerås Flaten, Ext groups in homotopy type theory [slides]
• Cipriano Junior Cioffo, Biased elementary doctrines and quotient completions [slides]
• Thorsten Altenkirch and Stefania Damato, Specifying QIITs using Containers [slides]
• Christopher Dean, Directed Types are Weak ω-Categories [slides]
• Ulrik Buchholtz, Tom de Jong and Egbert Rijke, On epimorphisms and acyclic types in HoTT [slides]
• Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu, Relating ordinals in set theory to ordinals in type theory [slides]
• Jarl G. Taxeraas Flaten, Dan Christensen, Ulrik Buchholtz and Egbert Rijke, Central H-spaces and banded types
• Jonas Frey, Duality for Clans and the Fat Small Object Argument [slides]
• Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand and Lars Birkedal, Controlling unfolding in type theory using extension types [slides]
• Perry Hart and Favonia, Colimits in the category of pointed types [slides]
• Ivo Herzog, Goursat Homology [slides]
• Felix Cherubini, Thierry Coquand and Matthias Hutzler, A Foundation for Synthetic Algebraic Geometry [slides]
• Tom Jack, π₄𝕊³ ≇ 1 and another Brunerie number in CCHM [slides]
• Samuel Lavenir, Hilton-Milnor’s theorem in higher categories [slides]
• Chaitanya Leena Subramaniam and Michael Shulman, The FOLDS theory associated to a contextual category [slides]
• Axel Ljungström, Symmetric Monoidal Smash Products in HoTT [slides] ***Best student paper award winner***
• Louis Martini and Sebastian Wolf, Internal higher topos theory [slides]
• David Jaz Myers, Orbifolds in Synthetic Differential Cohesive HoTT [slides]
• Thorsten Altenkirch and Jacob Neumann, Presheaf Models of Polarized Higher-Order Abstract Syntax [slides]
• Egbert Rijke, The agda-unimath library [slides]
• David Jaz Myers and Mitchell Riley, Commuting Cohesions [slides]
• Robert Rose, Matthew Weaver and Daniel Licata, Deciding the cofibration logic of cartesian cubical type theories [slides]
• Matteo Spadetto, Propositional dependent type theories: a conservativity result for homotopy elementary types [slides]
• Samuel Speight, Groupoidal Realizability Over an Untyped Cubical Lambda-Calculus [slides]
• Andrew Swan, Oracle modalities [slides]
• Elif Uskuplu, Cofibrancy of The Exo-type of Natural Numbers [slides]
• Daniel R. Licata and Matthew Weaver, Theory and Implementation of Bicubical Directed Type Theory
• Jonathan Weinberger, Internal sums for synthetic fibered (∞,1)-categories [slides]
• Errol Yuksel, On the logic of sets in the simplicial model [slides]

Social events

• On Monday at 18:00 there will be a barbecue at the Vietnam Veterans Pavillion in Schenley Park.
• We will hold a reception at the Schenley Visitor Center on Wednesday at 17:30.