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