Abstract is missing.
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- Mendler Dialgebras and Recursion Schemes of Mixed VarianceStephan Alexander Spahn. [doi]
- HoTT OperadsBrandon Hewer, Graham Hutton. [doi]
- Functional Representability in Local Set TheoriesEnrique Ruiz Hernández, Pedro Solórzano. [doi]
- Symmetries in SortingVikraman Choudhury, Wind Wong. [doi]
- Towards Fuzzy Constructive Type TheoriesBesik Dundua, Furio Honsell, Temur Kutsia, Marina Lenisa, Luigi Liquori. [doi]
- Kleisli Categories with Display MapsMoana Jubert. [doi]
- A Data Type of Intrinsically Plane Graphs in AgdaMalin Altenmüller, Conor Titania McBride. [doi]
- The Rezk Completion for Elementary TopoiKobe Wullaert, Niels van der Weide. [doi]
- Nominal Type Theory by Nullary Internal ParametricityAntoine Van Muylder, Andreas Nuyts, Dominique Devriese. [doi]
- Lean4Lean: Verifying a Typechecker for Lean, in LeanMario Carneiro. [doi]
- A Graded Modal Type Theory for Pulse SchedulesRobin Adams 0001, Jean-Philippe Bernardy, Lorenzo Perticone, Jeremy Pope. [doi]
- Multi-Clocked Guarded Recursion Beyond ωRasmus Ejlers Møgelberg. [doi]
- Formalisation and Extension of Lagois Connections for Secure Information FlowCasper Ståhl, Léon Gondelman, René Rydhof Hansen, Danny Bøgsted Poulsen. [doi]
- Choice Principles and Hypercompletion in HoTTOwen-Milner. [doi]
- Type-Theoretic Replacement and Univalent Completion: Applications and InterpretationsEvan Cavallo, Thierry Coquand. [doi]