Kapulkin : Π-types and Σ-types in homotopy theoretic models of type theory

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

Les types dépendants sont abordés dans le Livre, voir :

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/16/hott-the-book-1-4-dependent-function-types-π-types/

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

Ce travail de Kapulkin sous forme de transparents aborde le lien avec les catégories:

https://www.mathstat.dal.ca/~selinger/ofest2010/slides/Kapulkin-Pi_and_Sigma_slides.pdf

La page 3 sur 17 donne les équivalences pour Π et Σ dans les trois domaines de la théorie des types, de celle des ensembles ( où les correspondants sont le produit cartésien et le coproduit) et la logique ( où ce sont les deux quantificateurs, universel et existentiel, qui correspondent respectivement au
Π Et Σ-type)

Les deux pages suivantes (4 et 5) donnent les règles de formation, d’introduction, d’élimination et de calcul (COMP) respectivement pour les Π et Σ-types.

Un exemple de formation est donné Page 6 suivante pour le type Nat des entiers naturels et le type dérivé:

n:Nat ⊢ Rn: Type

Puis les notes abordent la sémantique des Lccc ( locally cartesian closed categories)

https://proofwiki.org/wiki/Definition:Pullback_Functor

Les catégories localement…

Voir l’article original 180 mots de plus

Publicités

Répondre

Entrez vos coordonnées ci-dessous ou cliquez sur une icône pour vous connecter:

Logo WordPress.com

Vous commentez à l'aide de votre compte WordPress.com. Déconnexion /  Changer )

Photo Google

Vous commentez à l'aide de votre compte Google. Déconnexion /  Changer )

Image Twitter

Vous commentez à l'aide de votre compte Twitter. Déconnexion /  Changer )

Photo Facebook

Vous commentez à l'aide de votre compte Facebook. Déconnexion /  Changer )

Connexion à %s