8:30 - 9:00 Coffee and
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:00CoffeeCoffeeCoffeeCoffee
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:00LunchLunchLunchLunch
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
The 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:00CoffeeCoffeeCoffeeCoffee
16:00 - 16:30
SwanOracle modalities
GratzerControlling unfolding in type theory using extension types
ShulmanThe 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:00Reception
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

Vladimir Voevodsky memorial lecture

Contributed talks

Social events