#HoTT, théorie des catégories et des ensembles (ZFC)

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

Cet article « Univalent higher categories via complete semi-Segal types »:

https://arxiv.org/pdf/1707.03693.pdf

rappelle en Page 2 sur 31 que toutes les approches des catégories multidimensionnelles (higher categories) ont un point commun qui est d’utiliser les ensembles comme « building blocks » , exploitant ainsi le caractère fondationnel de la théorie des ensembles avant la naissance de la théorie des catégories en 1945.

Dans la terminologie de ce blog, cela signifie que le plan internel est bâti avec les briques du plan ontologique.

Mais la théorie homotopique des types ne conçoit pas les ensembles comme des collections, comme le font les théories axiomatiques des ensembles telles ZFC, mais à la manière des théories de l’homotopie, nettement mieux adaptées à la théorie des catégories et à sa notion d’équivalence. Dans ce cadre les ensembles sont simplement des 0-catégories, sans morphismes non triviaux, et pour HoTT ce sont des 0-types , sans chemins autres que triviaux entre…

View original post 113 more words

Advertisements

Elementary (∞,1)-topoi

#HoTT : The Book; homotopies et équivalences

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

The HoTT Book

Paragraphe 2.4 page 76

Au fond c’est le sujet central de la théorie homotopique des types, celui des rapports entre identité (égalité) et indiscernabilité:

https://anthroposophiephilosophieetscience.wordpress.com/2017/12/18/andrei-rodin-identity-equality-and-equivalence-in-mathematics/

https://anthroposophiephilosophieetscience.wordpress.com/2017/12/20/identite-des-indiscernables/

https://www.sussex.ac.uk/webteam/gateway/file.php?name=talk.pdf&site=552

https://anthroposophiephilosophieetscience.wordpress.com/2017/12/20/hott-equality-indistinguishabity/

https://uberty.org/wp-content/uploads/2017/06/synhott-shulman.pdf

What’s Special About Identity Types

C’est par là que les types peuvent être vus comme des ∞-groupoides, c’est à dire comme des objets de ∞Grpd, qui est une (∞,1)-catégorie, c’est à dire ici une Idée, un objet de (∞,1)Cat et l’exemple paradigmatique d’un ∞-topos, l’analogue du 1-topos Set, Idée de l’être , sous-catégorie de Cat qui est Idée de l’Idée

https://anthroposophiephilosophieetscience.wordpress.com/2016/08/25/la-metacategorie-cat-de-toutes-les-categories-comme-modele-mathematique-du-monde-des-idees-de-platon/

https://anthroposophiephilosophieetscience.wordpress.com/2016/08/22/premiere-pierre-pour-une-nouvelle-science-internelle-mathesis-universalis-lidee-de-lun/

http://alpha.math.uga.edu/~davide/The_Category_of_Categories_as_a_Model_for_the_Platonic_World_of_Forms.pdf

Mais revenons au Livre « Homotopy type theory » paragraphe 2.4 page 76

Le type x =A y , appelé Type identité (identity type) peut être vu comme chemin (path) ou équivalence entre deux éléments (deux points d’un espace ) x et y du type A.

L’axiome d’univalence nous assure que nous avons le droit d’identifier ces…

View original post 178 more words

UCR : exposés sur la théorie appliquée des catégories