| CARVIEW |
Workshop on Homotopy Type Theory/ Univalent Foundations
July 7-8, 2018, Oxford, United Kingdom.
Co-located with FSCD 2018 and part of FLoC 2018.
Quick info
- Link to the program
- Location: Blavatnik School of Government, Radcliffe Observatory Quarter, Woodstock Road (Google map)
Overview
Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory.
The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory/Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory.
Details regarding registration, accommodation and all other practical matters can be found on the main FLoC site. FLoC also provides travel stipends for students with application deadline May 18.
Invited speakers
- Martín Escardó (University of Birmingham):
Injective types and searchable types in univalent
mathematics [slides]
Abstract: We characterize the injective types as the retracts of exponential powers of the universes. The injective (n+1)-types are the retracts of the universes of n-types, and in particular the injective sets are the retracts of powersets. We apply this to construct searchable types, with the property that every decidable subset has an infimum in a well founded, transitive, extensional order. This applies Yoneda-style machinery for types seen as infty-groupoids.
- Paige North (Ohio State University), joint with
HDRA:
A homotopy type theory for directed homotopy theory
Abstract: In this talk, I will propose a directed type theory. The goal of this project is to develop a type theory which can be used to describe directed homotopy theory and category theory. At the core of this type theory is a `homomorphism’ type former whose terms are meant to represent homomorphisms or directed paths. Its rules are roughly analogous to those of Martin-Löf’s identity type. I will give an interpretation of this type former in the category of small categories which helps to elucidate its rules. I will also describe progress towards constructing weak factorization systems and interpretations in categories of directed spaces.
- Andrew Pitts (University of Cambridge):
Axiomatizing Cubical Sets Models of Univalent
Foundations [slides]
Abstract: The constructive model of Homotopy Type Theory introduced by Cohen-Coquand-Huber-Mörtberg in 2015 (building on the work of Bezem-Coquand-Huber in 2013) uses a particular presheaf topos of cubical sets. It is arguably one of the most significant contributions to constructive mathematics since Martin-Löf's work in the 1970s. Since its introduction, much effort has been expended to analyse, simplify and generalize what makes this model of the univalence axiom tick, using a variety of techniques. In this talk I will describe an axiomatic approach -- the isolation of a few elementary axioms about an interval and a universe of fillable shapes that allow a univalent universe to be constructed. Not all the axioms are visible in the original work; and the axioms can be satisfied in toposes other than the original presheaf topos of cubical sets. The axioms and constructions can almost be expressed in Extensional Martin-Löf Type Theory, except that the global nature of some of them leads to the use of a modal extension of that language. This is joint work with Ian Orton, Dan Licata and Bas Spitters.
Program
The schedule can be found here. The accepted contributed talks are:- Andreas Nuyts and Dominique Devriese: Internalizing Presheaf Semantics: Charting the Design Space (abstract | slides)
- Andreas Nuyts: Robust Notions of Contextual Fibrancy (abstract | slides)
- Andrei Rodin: Univalent Foundations and the Constructive View of Theories (abstract | slides)
- Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Møgelberg, Andrew Pitts and Bas Spitters: Dependent Right Adjoint Types (abstract | slides)
- Clive Newstead: Algebraic models of dependent type theory (abstract | slides)
- Taichi Uemura: Cubical Assemblies and the Independence of the Propositional Resizing Axiom (abstract | slides)
- Iosif Petrakis: A Yoneda lemma-formulation of the univalence axiom (abstract | slides)
- Edward Morehouse: Ordered Cubes (abstract | slides)
- Eric Faber: Towards a geometric model theory of type theory (abstract)
- Jonathan Weinberger and Ulrik Buchholtz: (Truncated) Simplicial Models of Type Theory (abstract | slides)
- Thorsten Altenkirch: Towards the syntax and semantics of higher dimensional type theory (abstract | slides (talk given by Nicolai Kraus))
- Genki Sato: Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT (abstract)
- Joseph Helfer: First-order homotopical logic and Grothendieck fibrations (abstract)
- Felix Wellen: Cohesive Covering Theory (abstract | slides)
- Kuen-Bang Hou (Favonia), Carlo Angiuli, Evan Cavallo, Robert Harper and Jonathan Sterling: Computational Cubical Type Theory (abstract | slides)
- Hugo Herbelin: The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval (abstract)
Submissions
Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via EasyChair.
- Abstract submission deadline: April 15
- Author notification: end of April
Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work.
Organisers
- Benedikt Ahrens,
B.Ahrens at cs.bham.ac.uk(University of Birmingham) - Simon Huber,
simon.huber at cse.gu.se(University of Gothenburg) - Anders Mörtberg,
mortberg at cmu.edu(Carnegie Mellon University and University of Gothenburg)
Program committee
- Benedikt Ahrens (University of Birmingham)
- Paolo Capriotti (University of Nottingham)
- Simon Huber (University of Gothenburg)
- Chris Kapulkin (University of Western Ontario)
- Nicolai Kraus (University of Nottingham)
- Peter LeFanu Lumsdaine (Stockholm University)
- Assia Mahboubi (Inria Saclay)
- Anders Mörtberg (Carnegie Mellon University and University of Gothenburg)
- Nicolas Tabareau (Inria Nantes)
Special issue
We are soliciting submissions for a Special Issue of the journal