July 7-8, 2018, Oxford, United Kingdom.
Co-located with FSCD 2018 and part of FLoC 2018.
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.
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.
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.
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.
Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via EasyChair.
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.
B.Ahrens at cs.bham.ac.uk
(University of Birmingham)simon.huber at cse.gu.se
(University of Gothenburg)mortberg at cmu.edu
(Carnegie Mellon University and University of Gothenburg)