Monthly Archives: December 2017

#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/

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/

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 trois notions…

View original post 176 more words

T. Streicher : a model of type theory in simplicial sets