Univalent categories and The Rezk completion

Voir aussi cet exposé sur la formalisation de la théorie des catégories en théorie des types:

http://benedikt-ahrens.de/talks/IHP_Ahrens.pdf

ainsi que Displayed categories:

https://arxiv.org/abs/1705.04296

Et « Categorical structures for Type theory »

https://arxiv.org/abs/1705.04310

https://ncatlab.org/nlab/show/Benedikt+Ahrens

Commençons donc à étudier ces notes d’exposé d’un travail de B. Ahrens, Kapulkin et Shulman

https://www.irit.fr/TYPES2013/Slides/TYPES13Slides_Ahrens_et_al.pdf

en tout cas la partie introductrice qui a la même vertu que les travaux de Joyal : mettre à jour les relations entre HoTT et théorie des catégories et théorie des catégories multidimensionnelles (higher categories).

Cela commence à la page 2 « trois sortes d’identité -sameness pour les catégories :

Égalité C= D : il s’agit de la même catégorie

Isomorphisme C ≌ D ce qui indique que les deux catégories peuvent être reliées par deux foncteurs inversibles, inverses l’un de l’autre

https://fr.m.wikipedia.org/wiki/Isomorphisme_de_catégories

Équivalence :

C ≃ D ce qui est une propriété un peu plus faible (lax, weak) que l’isomorphisme

https://fr.m.wikipedia.org/wiki/Équivalence_de_catégories

Toute la puissance de l’axiome d’univalence consiste à confondre ces trois notions.

Page 4 sur 23 : Les sigma-types ∑x:AB(x), product-types Πx:A B(x) et identity-types IdA(a,b) sont mis en relations avec les notions catégoriques-homotopiques : espace total, espace de sections, espace des chemins, voir l’article précédent :

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/20/differentes-notes-dandre-joyal-sur-la-description-categorique-de-hott/

Ces types et leurs règles de formation sont évidemment traités dans le Livre « Homotopy type theory »

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/27/hott-the-book-product-types-dependent-pair-types-ou-σ-type/

Page 7 sur 23 « Level of a Type » les propositions ou (-1)-types sont les type A pour lesquels deux termes quelconques sont égaux :

a,b:A a = b

On associe à A le Type

IsProp(A)= Π x,y:A Id (x,y)

le type A est une proposition si le type IsProp(A) est habité ( a un élément)

Le type A est un ensemble si pour tous x,y:A le Type Id(x,y) est une proposition d’où le type associé:

IsSet (A)=Πx,y:AIsProp(Id(x,y))

Le produit Π dans HoTT correspond au signe logique ∀ pour « quel que soit » , la somme sigma Σ au signe logique ∃ pour « il existe » . rappelons que ces deux quantificateurs logiques , respectivement appelé quantificateur universel et quantificateur existentiel:

https://ncatlab.org/nlab/show/universal+quantifier

https://ncatlab.org/nlab/show/existential+quantifier

prennent la forme catégorique de deux foncteurs adjoints (sur une idée de William Lawvere)

https://math.stackexchange.com/questions/467640/categorical-interpretation-of-quantification

Une équivalence de deux types A et B est une fonction

f: A → B

avec les propriétés données Page 7

Les équivalences entre deux types A et B forment un type noté Equiv(A,B); l’axiome d’univalence identifie ce type à Id(A,B) voir page 5 de

https://www.irit.fr/TYPES2013/Slides/TYPES13Slides_Ahrens_et_al.pdf

Une catégorie est définie dans le cadre de HoTT/UF par un type des objets et pour chaque couple d’objets un ensemble (un type qui est un ensemble) des morphismes page 11 et 14
Page 15 est définie la propriété d’être un isomorphisme: c’est une proposition pour un morphisme f, notée IsIso(f)

Le type isomorphisme entre deux objets est alors un sigma-type :

Iso (a,b) = ∑f:C(a,b) IsIso(f)

Page 8 sur 23 est définie une fonction entre types, notée

Id_to_Equiv(A,B) : Id (A,B) → Equiv (A,B)

refl (A) → (a —-> a)

refl vient de reflexive c’est l’identité entre points ou types, le chemin qui reste immobile

l’axiome d’univalence s’ecrit alors :

Univalence : ΠA,B:UIsEquiv(Id_to_Equiv(A,B))

ce qui se lit : quels que soient les types A , B dans l’univers U , l’équivalence de A et B est équivalente à leur identité (puisque comme il a été dit le produit Π correspond au quantificateur universel en logique)

On note :

p: x ⤳ y p est un chemin menant de x à y , une preuve que x égal à y

pour p: IdA(x,y)

Page 16 sont définies les catégories univalentes

On considère deux objets a , b de la catégorie définie dans le cadre de la théorie des types. Ce sont des termes du type des objets .
Définition de la fonction entre types :

id_to_Iso(a,b) : (a ⤳ b) → Iso (a,b)

refl(a) → Id a
refl(a) est le chemin de a à a (on ne bouge pas)
La catégorie est dite univalente si pour tout couple a, b d’objets il s’agit d’une équivalence de types

Dans une catégorie univalente les objets isomorphes sont égaux.

« C est une catégorie univalente » est une proposition, notée

IsUniv(C)

Des exemples de catégories univalentes sont donnés page 17:

Set la catégorie des ensembles

Les catégories de structures algébriques (groupes, anneaux)

Les sous-catégories pleines de catégories univalentes

https://ncatlab.org/nlab/show/full+subcategory

Si D est univalente, la catégorie , notée DC de foncteurs de C vers D, est univalente

Les catégories univalentes sont incluses dans la 2-catégorie des catégories , ce foncteur d’inclusion a un adjoint à gauche, qui est appelé complétion de Rezk .

En référence le texte indique l’article de Rezk : « A model for the homotopy theory of homotopy theory »

https://arxiv.org/pdf/math/9811037.pdf

Advertisements
This entry was posted in ∞-catégories, homotopy type theory. Bookmark the permalink.