Abstracts, Computational Aspects of Univalence 2016
Computational Aspects of Univalence,
Workshop in Bergen, January 20-22, 2016
Marc Bezem, Overview of the project Computational Aspects of Univalence
We present the scientific objectives of the project by going through a series of case studies. The first two have actually been started, the others are only planned. We encourage active participation of the audience in this talk, and in particular in the subsequent discussion session. The idea is that the project can benefit a lot from the experience of others, avoiding pitfalls and/or dead ends, choosing the most promising approach, or even undertaking a completely different case study.
Thierry Coquand, Some higher-inductive types in a cubical set model
This talk will be a complement to Simon's mini-course. We explain how
to give a semantics to the spheres and to propositional truncation. I will also comment
on the recent work of Andrew Swan and how to recover an identity type equivalent
to, but not judgmentally equal to, the path type.
Peter Dybjer, Game Semantics and Normalisation by Evaluation
Game semantics and normalization by evaluation have both been active fields of research since the 1990s. In game semantics computation a program is thought of as a player playing a game against the enviroment. Among other things game semantics has been proposed as a solution to the long standing full abstraction problem in semantics. Normalization by evaluation on the other hand is a technique for computing normal forms in lambda calculi by interpreting terms in a model and then "reifying" the result. We shall here show a new way to present Hyland and Ong's game semantics for PCF by using normalization by evaluation (nbe). We use the bijective correspondence between innocent well-bracketed strategies and PCF Bohm trees, and show how operations on PCF Bohm trees, such as
composition, can be computed lazily and simply by nbe. The usual equations characteristic of games follow from the nbe construction without
reference to low-level game-theoretic machinery. As an illustration, we give a Haskell program computing the application of innocent strategies.
(joint work with Pierre Clairambault, CNRS, ENS Lyon).
Martin Escardo, Infinite types that satisfy the principle of omniscience
Assuming function extensionality, many infinite types X satisfy (Pi(p:X->2).(Pi(x:X).p(x)=0)+(Sigma(x:X).p(x)=1)) constructively. Among them, several are ordinals, again in a constructive sense. A certain construction F:(N->U)->U builds an omniscient type out of countably many omniscient types. Applying it to a constant sequence of types, we get G:U->U. The final coalgebra of G is the Cantor type (N->2). Its initial algebra consists of binary sequences that have finitely many zeros in a suitable sense (to be elucidated).
UniMath is a project initiated by Vladimir Voevodsky whose goal is to formalize
a substantial amount of mathematics, thereby verifying the proofs and making
them usable in further formalization and in research. The basis for the formalization is the Univalent Foundations, which can be viewed as a foundation of mathematics tailored directly to the use of Martin-Löf type theory in Coq. I will give an introduction to the project and its code, aiming to help those interested in exploring it, extending it, or using it, to acquire the basic skills to navigate its proofs. I'll also offer various hints about efficient use of "emacs" and "ProofGeneral".
Simon Huber, Minicourse on Cubical Type Theory
Cubical type theory is an extension of dependent type theory which
allows to directly argue about n-dimensional cubes (points, lines,
squares, cubes etc.). It is based on a model of dependent type theory
in cubical sets given in a constructive meta theory. The type theory
allows for new ways to reason about the identity type, e.g., function
extensionality as well as Voevodsky's Univalence Axiom become
provable. In this course I will explain the system with a focus on
its computational aspects and show how the Univalance Axiom can be
deduced. This is joint work with Cyril Cohen, Thierry Coquand, and
A. Polonsky, Equality by induction on type structure
We discuss the problem of extensionality from the syntactic viewpoint.
Specifically, we report on the program of defining HoTT-style extensional equality as the canonical logical relation on the term model of type theory.
At first, we shall treat the concept of logical relations, paying attention to the subtleties which arise when passing to dependent types. For the type system lambda-*, we show how the term model can be described using the language of inductive-recursive definitions, and how the relation representing equality can be captured by a generalization of such definitions.
In the next step, the previous construction must be internalized in such a way that the invariance properties of equality are witnessed by terms in the same system. We construct a universe closed under "its own" logical relation.
Finally, we will discuss the problems which arise when the invariance operator is itself internalized, and when we try to account for the remaining properties of equality. These naturally point to the nominal ideas which play an important role in cubical type theory.