Marc Lasson
University of Cambridge
https://who.rocq.inria.fr/Marc.Lasson/
Date(s) : 18/04/2014 iCal
11 h 00 min - 12 h 00 min
The synthetic approach to weak ω-groupoids promoted by the univalent foundation program is the idea that (homotopy) type theory should be the primitive language in which spaces, points, paths, homotopies are derived. Following this approach, spaces are represented by types, points by inhabitants and paths by equalities between points (also known as identity types) and algebraic properties of these objects should not be unforced a priori (for instance by axioms) but should be derived directly from the language. Following this approach requires to be convinced that definitions of new operations should be canonical, in the sense that no important choice should be made by picking an implementation of these operations instead of an other. Identities, inversion and concatenation of path, associativities, idempotency of inversion, horizontal and vertical compositions of 2-paths, are all examples of groupoid laws.
Parametricity has been introduced by Reynolds to study the polymorphic abstraction of system F. It refers to the concept that well-typed programs cannot inspect the type their arguments; they must behave uniformly with respect to abstract types. Reynolds formalizes this notion by showing that polymorphic programs satisfy the so-called logical relations defined by induction on the structure of types. Dependent type systems are expressive enough to state their own parametricity theory.
In this talk, we will focus on the consequences of this remark when applied to identity types and we will use it to prove that all implementations of a given groupoid law are provably equal to each other.
http://www.cl.cam.ac.uk/~mrl42/
Catégories