#HoTT : André Joyal retour sur les règles de formation, d’introduction, d’élimination et de calcul

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

Ces notes d’andré Joyal :

http://logica.dmi.unisa.it/tacl/wp-content/uploads/2014/08/Joyal-TACL2015.pdf

Reviennent sur ces règles, en pages 10 à 12 sur 39

Ces règles très importantes et qui reviennent à tout bout de champ sont expliquées dans The Book :

The HoTT Book

Page 27 , au paragraphe 1.5 « product types » , voir aussi cet article :

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

« 1 règles de formation, expliquant comment former ce nouveau genre de types

Exemple : si A, B sont des types, on peut former le type des fonctions :

A → B
2 “constructeurs” (constructor “), règles d’introduction : comment former les éléments de ce nouveau type

Exemple : une seule règle pour les types de fonction, la λ-abstraction

3 les “éliminateurs” ou règles d’élimination, expliquant comment utiliser les éléments de ce nouveau type Exemple : le type des fonctions a une seule régle d’élimination, l’application d’une fonction.

4 les règles de calcul (computation rules) :comment un…

View original post 532 mots de plus

Publicités