#HoTT The Book 1.12 identity types

The HoTT Book

Aller à 1.12 page 47

Conformément à la thèse «  propositions as types » la proposition assertant l’égalité de deux éléments a, b appartenant à un même type A , est elle même un type, appelé identity type ou equality type, et noté IdA(a,b)

Une égalité entre deux termes à et b est un chemin (path) reliant à et b , et un « identity type » est donc un « path object » dans la catégorie des types. Ceci est le point de vue de la théorie de l’homotopie:

What’s Special About Identity Types

Un « identity type » est un exemple d’un « inductive type »

https://arxiv.org/pdf/1201.3898.pdf

https://ncatlab.org/nlab/show/identity+type

La page Nlab précédente donne une définition en termes de règles de formation , d’introduction, d’élimination et de calcul (computation rules) comme il est expliqué dans The Book

Page 27 au 1.5 « Product types » voir:

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

mais la page Nlab donne aussi l’explication en termes de « inductive types », comme on en donne la raison au dessus, c’est à dire que le type A (identity type) est engendré de façon inductive par les équations dites de réflexivité (x=x) de même que le type des entiers naturels par 0 et la fonction successeur. Tel est le sens de la formule dans le logiciel Coq:

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

La réflexivité n’est autre que l’opération de l’Un , exprimée dans la théorie des catégories par l’opérateur Id qui peut être un morphisme ou un foncteur, qu’Alain Badiou par idéologie négatrice de l’Un ramène au « compte-Pour-Un » ensembliste , ce que la philosophie d’African Spir qui a grandement influencé Brunschvicg interprète mieux ( à mon sens ) en montrant que l’identité d’une substance est en nous une notion qui vient d’ailleurs que du monde : aucune substance qui existe n’est identique à soi même, cette loi logique de notre pensée n’est donc pas découverte et « en provenance » du monde. Dans le système de Bolzano cela correspond aux substances (objets) ou aux adhérences (qualités):

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/09/le-langage-du-systeme-de-bolzano-1/

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/09/le-langage-du-systeme-de-bolzano-1/

qui seules existent ( dans le monde) alors que les idées du plan « lectologique » n’existent pas . Dans le système de ce blog, le monde correspond au plan ontologique , et le plan lectologique de Bolzano au plan internel et à la mathématique des catégories ou des ∞-catégories. Les types dans HoTT unissent les deux plans, d’ailleurs la théorie homotopique des types réunit les deux versants, celui de la Science (théorique) et celui de la techno – Science (programmation, » computer science »)

A cela on voit que la théorie homotopique des types, qui est au fond, comme le montrent les travaux d’André Joyal, pour ce qui est de son versant théorique, une autre version de la théorie des catégories , est un langage possible pour la Science Internelle, cette « physique «  du monde internel des Idées, c’est à dire du plan de l’Un d’où s’origine La loi de la pensée humaine de l’identité. L’être Humain n’est pas le « berger de l’être mais le Hérault de l’Un » , ceci soit dit à la fois aux heidegerriens et aux badiolistes qui, en politique, correspondent à l’extrême Droattte et a l’extrême Gauche islamo- kollabo .

Plusieurs pages du Nlab sur ce lien étroit entre théorie des catégories et logique ou HoTT:

https://ncatlab.org/nlab/show/categorical+semantics

https://ncatlab.org/nlab/show/categorical+model+of+dependent+types

https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory

https://ncatlab.org/nlab/show/type-theoretic+model+category

Page 48 : la réflexivité est une fonction (« dependent function »)

refl : Πa:A(a=a)

qui asserte que tout élément de A est identique à lui même.

refla est appelé « chemin constant » au point a.

La notion d’ »identity type » est à mon avis la plus importante dans HoTT:

Awodey, Warren: Homotopy theoretic models of identity types

Advertisements
This entry was posted in Alain Badiou, Cochet-Brunschvicg, homotopy type theory, Léon Brunschvicg, Ouvert : dualité plan vital-plan spirituel, Philosophie, Science-internelle. Bookmark the permalink.