#HOTT The Book : théorie des catégories et des précatégories

The HoTT Book

Je saute d’un seul coup au chapitre 9 du livre page 317, parce que la formalisation de la théorie des catégories dans le cadre de la théorie homotopique des types est le point le plus crucial au point où nous en sommes arrivés :

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/26/definition-des-∞1-categories-dans-le-cadre-de-hott/

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/31/hott-levenement-spirituel-de-la-theorie-homotopique-des-types/

https://anthroposophiephilosophieetscience.wordpress.com/2018/02/05/hott-theorie-homotopique-des-types-∞-cosmoi-et-∞-categories-vers-la-scienceinternelle/

J’ai distingué depuis le début entre, non pas deux mathématiques, il n’y en a qu’une seule, mais deux cadres pour la mathématique :

https://mathesisuniversalis2.wordpress.com/2015/06/09/les-deux-formalismes-mathematiques-de-badiou-theorie-des-ensembles-et-theorie-des-topoi/

https://anthroposophiephilosophieetscience.wordpress.com/2016/03/15/les-deux-theories-mathematiques-privilegiees-par-badiou-topoi-et-ensembles-correspondant-aux-deux-plans-vital-ontologique-et-spirituel/

qui sont au stade ultime dans une position de dualité qui est celle de l’Ouvert : la dualité de l’être et de l’Un

https://coranetmathesis.wordpress.com/franck-jedrzejewski-diagrammes-et-categories-lun-comme-dual-de-letre/

https://anthroposophiephilosophieetscience.wordpress.com/2018/02/12/resume-de-la-these-de-frank-jedrzejewski-diagrammes-et-categories-lun-comme-dual-de-letre/

A ces deux cadres mathématiques correspondent deux universalismes, concret et abstrait :

https://mathesisuniversalis2.wordpress.com/deux-universalismes-concret-categorique-henologique-et-abstrait-ensembliste-ontologique/

Cette distinction mathématique a une importance cruciale pour la question religieuse :

https://coranetmathesis.wordpress.com/application-de-la-these-des-deux-universalismes-mathematiques-aux-trois-monotheismes-abrahamiques/

Et si Badiou refuse l’Un avec une violence particulière en se revendiquant comme athée, c’est peut être parce qu’il n’admet que l’universalisme abstrait et ontologique des ensembles, c’est à dire d’une catégorie particulière Set qui est un topos, LE paradigme de la notion de topos , où l’Un n’est présent que comme opération, comme « compte-Pour-Un » ensembliste, alors qu’il joue le rôle de morphisme-identité pour toute catégorie . Et la théorie des types ? L’Un s’y trouve aussi (où ne se trouverait il pas?) comme type -identité (identity type )

https://mathesismessianisme.wordpress.com/2017/10/14/path-categories-and-propositional-identity-types/

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/14/a-category-theoretic-version-of-the-identity-type-weak-factorization-system/

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/24/hott-the-book-1-12-identity-types/

L’interaction de la théorie des catégories CT et de la théorie homotopique des types HOTT forme donc le cœur même de la Science internelle recherchée ici, comme schéma enfin rigoureux de la « science recherchée », la métaphysique.

https://golem.ph.utexas.edu/category/2013/03/category_theory_in_homotopy_ty.html

Higher Lenses

Ross Street : categorical structures

http://maths.mq.edu.au/~street/45.pdf

Le paragraphe 9.1 du livre commence par opposer catégories et précatégories, la définition est donnée en 9.1.1 et est pratiquement la même que celle de catégorie

https://hottandphilosophy.wordpress.com/2018/02/19/2-categories-vs-precategories/

Il y a un type des objets et pour les flèches une famille de types indexée sur les objets . Les types de morphismes sont des ensembles.

Le lemme 9.1.4 définit pour tout couple d’objets d’une précatégorie la fonction:

idtoiso : (a=b) → (a≅b)

Une catégorie est alors définie en 9.1.6 comme une précatégorie pour laquelle cette fonction est une équivalence .

Dans une catégorie, si (a≅b) alors (a=b)

On en déduit au lemme 9.1.8 que pour toute catégorie le type des objets est un 1-type

https://anthroposophiephilosophieetscience.wordpress.com/2017/11/06/hott-n-types/

idtoiso a un inverse :

isotoid : (a≅b) → (a=b)

L’exemple 9.1.14 définit un préordre comme une précatégorie pour laquelle tout ensemble Hom (a,b) est une proposition, c’est à dire un (-1)-Type:

https://ncatlab.org/nlab/show/homotopy%20n-type

De manière équivalente c’est un type muni d’une relation ≤ réflexive et transitive.
Un ordre partiel (noté en anglais poset) est alors une catégorie, où (a≅b) est la pure proposition que a≤b et b≤a

Tout type (a=b) y est une pure proposition, un (-1)-type et il existe une fonction

(a≅b) → (a=b)

Le type des objets est un ensemble muni d’une relation ≤ antisymétrique :

a ≅ b si et seulement si a ≤ b et b ≤ a

9.1.15 :si A est une catégorie , le type des objets est un ensemble si et seulement si (a≅b) est toujours une pure proposition. C’est équivalent à : tout isomorphisme est une identité. Une telle catégorie est appelée « gaunt category »:

https://ncatlab.org/nlab/show/gaunt+category

C’est une propriété plus forte que celle de catégories squelettiques (skeletal category):

https://ncatlab.org/nlab/show/skeleton

Advertisements
This entry was posted in ∞-catégories, category theory, Higher category theory, homotopy type theory, Philosophie mathématique, Science-internelle. Bookmark the permalink.