L’argument du petit objet est une recette pour construire des factorisations de morphisme f:X \to Y en f=R(f)L(f) où L(f) et R(f) sont dans des classes L et R qui ont des propriétés de relèvement non-unique (orthogonalité faible) entre elles. Lorsque la propriété de relèvement de L et R est unique (orthogonalité forte) l’argument doit être modifié pour produire la bonne factorisation. Le but de l’exposé sera de proposer deux méthodes pour corriger la construction (inspirées de Gabriel-Ulmer et de Kelly).

Je partirai de deux “théorèmes” faux : Le premier est dû à Kapranov et Voevodsky et dit essentiellement que l'on peut représenter les types d'homotopie par des infini-catégories strictes dont toutes les flèches sont faiblement inversibles. Le deuxième est la preuve par Johnstone et Carboni (et Batanin) que la catégorie des polygraphes est une catégorie de préfaisceaux.

Les deux énoncés sont faux pour des raisons très similaires : à chaque fois l'argument clé est l'argument de Eckmann-Hilton, c'est-à-dire le fait que la composition des endomorphismes de n'importe quelle identité dans une infini-catégorie est strictement commutative. Cette commutativité est incompatible avec les deux affirmations précedentes.

Pour cette raison, il est conjecturé que si l'on travaille dans une situation où il n'y pas d'unité, ou bien où les unités sont faibles ou n'interviennent pas alors ces énoncés deviennent vrais. Dans le premier cas il s'agit de la conjecture de semi-strictification de Simpson qui affirme que les types d'homotopie peuvent être représentés par des infini-catégories strictes “sans identités” qui admettent des identités faibles et des inverses faibles. Dans le deuxième cas il s'agit d'une “conjecture” de Johnstone et Carboni qui dit que la catégorie des polygraphes tels que la source et le but de chaque générateur n'est pas une identité est une catégorie de préfaisceaux.

Dans l'exposé je présenterai une preuve de cette dernière “conjecture” et j'expliquerai en quoi cela pourrait permettre d'arriver à une preuve de la conjecture de Simpson.

We discuss the problem of equality in type theory. We present an approach to defining higher equality structures in type theory. As an application, we study the lambda calculus from the multi-dimensional point of view. Taking equality between lambda terms (1-cells) to be beta conversion modulo permutation of redexes, we discover that the induced higher structure is a homotopy 1-type. That is, whenever there exists a higher cell between two β-conversions, the space of such cells is contractible. The key property of the lambda calculus responsible for this is Lévy’s projection calculus (AKA calculus of residuals). We conclude that the result holds for any theory which admits a presentation with such a calculus. For example, all (weakly) orthogonal TRSs describe homotopy 1-types.

En 1953, S. Eilenberg et S. Maclane publient l'article “Acyclic Models” dans lequel ils exposent le théorème (ou méthode) dit des modèles acycliques. Cet outil permet de comparer efficacement différentes théories homologiques tout en étant très économe en calculs. Depuis, différents théorèmes dit de «modèles acycliques» ont été démontrés, comme par exemple celui de M.Barr et J. Beck en 1966. Pourtant même si ce dernier a des conclusions similaires au théorème d'Eilenberg et Maclane, le cadre semble assez différent. Dans mon exposé, je présenterai un théorème d'algèbre homologique très général duquel il est très facile de déduire ces différents théorèmes de modèles acycliques ainsi que les théorèmes habituels de relèvement d'algèbre homologique.

Je présenterai aussi mes travaux en cours qui visent à démontrer un théorème de relèvement plus fin et plus général que les précédents et dont un cas particulier a également été démontré par M. Barr dans les années 90. Enfin, si le temps me le permet, j'exposerai un théorème des modèles acycliques d'A. Prouté (non-publié) qui rentre naturellement dans ce nouveau cadre.

Dans son manuscrit “À la poursuite des champs” Grothendieck propose une définition “d'infini-groupoïde” ainsi qu'une notion d'équivalence entre eux et conjecture que la catégorie homotopique est équivalente à sa catégorie des infini-groupoïdes “à équivalence près”.

Cette conjecture (l'hypothèse d'homotopie) est toujours un problème ouvert, et il y a de très nombreuses questions basiques concernant cette notion d'infini-groupoïdes qui restent sans réponse. Pour cette raison, on préfère généralement utiliser les ensembles simpliciaux et les complexes de Kan pour définir la notion d'infini-groupoïde et servir de point de départ pour la théorie des catégories supérieures.

Cela dit l'apparition de la théorie homotopique des types nous donne de nouvelles motivations pour s'intéresser à cette notion d'infini-groupoïdes : tout d'abord n'importe quel type en théorie homotopique des types porte une structure d'infini-groupoïde au sens Grothendieck, ensuite, si la théorie des types est censée être la logique interne de certaines infini-catégories, il s'agit à priori d'infini-catégories globulaires, i.e. d'un genre plus proche de la définition de Grothendieck que des versions simpliciales. Enfin, on sait internaliser en théorie des types la définition d'infini-groupoïdes de Grothendieck, alors qu'on est très loin de savoir faire de même pour les approches simpliciales.

Dans cet exposé je vais présenter une nouvelle famille de définitions de la notion d'infini-groupoïde qui sont inspirées de celle de Grothendieck, et qui conservent certaines de ses bonnes propriétés, mais qui échappent aux problèmes de celle-ci et pour laquelle on sait en particulier prouver l'analogue de l'hypothèse d'homotopie.

On énoncera aussi une conjecture technique précise, d'apparence simple, qui impliquerait que la définition de Grothendieck est un cas particulier de la nôtre, et qui donc impliquerait aussi l'hypothèse d'homotopie et résoudrait une partie des problèmes ouverts concernant la définition de Grothendieck.

En me limitant aux (infini,1)-catégories, j’illustrerai pourquoi on a besoin des catégories supérieures. La réponse que je développerai est que certains axiomes formulables en théorie des catégories n’ont aucun modèles non-triviaux dans les catégories ordinaires mais pas dans les catégories supérieures. L’une de ces propriétés est « l’effectivité des colimites » (forme améliorée de la propriété d’univalence) qui est à la base des infini-topos. Un autre exemple est la propriété de « stabilité » qui simplifie drastiquement la compréhension et la manipulation de l’algèbre homologique.