18 avril 2014, 11:00 : Séminaire

Marc Lasson (Cambridge), Canonicity of groupoids laws using parametricity theory

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.

25 avril 2014, 11:00 : Séminaire

Laurent Poinsot (Paris 13), Sur le groupoïde de géométrie d'une variété équationnelle équilibrée

Patrick Dehornoy a construit un monoïde de fonctions partiellement définies sur une algèbre de termes sur un domaine d'opérateurs (signature) S, dit monoïde de géométrie, qu'il associe à toute variété équationnelle V de S-algèbres déterminée par une congruence équilibrée, i.e., pour laquelle deux termes équivalents possèdent les mêmes ensembles de variables. Dans cet exposé je dégagerai la nature profonde de cette construction qui est celle d'un groupoïde. Je montrerai que celui-ci n'est que l'image d'un groupoïde plus fondamental par une représentation fidèle (un foncteur fidèle dans le groupoïde des ensembles et bijections). Ce dernier gouverne alors la "géométrie" du calcul dans la variété V, au sens où son action sur un terme correspond à des réécritures (au sens de la réécriture de termes), et hérite de surcroît d'une structure fonctorielle de S-algèbre. Si le temps me le permet, j'aborderai la généralisation de cette construction obtenue en remplaçant l'algèbre des termes par une algèbre libre dans une variété équationnelle déterminée par une congruence "linéaire".