Archives quotidiennes :

#HoTT : Comprehension categories as 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 ενοσοφια μαθεσις

D’abord cet article axé sur les « comprehension categories « :

http://www.cs.nott.ac.uk/~psxpc2/report-2013.pdf

puis cet exposé de Michael Shulman :

https://home.sandiego.edu/~shulman/hottseminar2012/05categories.pdf

(Cf page 3 la définition de display map category)

Et cet autre article :

https://ac.els-cdn.com/S1571066108000431/1-s2.0-S1571066108000431-main.pdf?_tid=6ae513c2-45bf-4641-820e-85f126850e32&acdnat=1520157026_ef815d3183b0c1afb49272a9aa0c2e4a

http://enslyon.free.fr/rapports/info/Alexandre_Buisse_3.pdf

http://philomatica.org/wp-content/uploads/2016/12/models.pdf

La méthode la plus simple consiste à partir des catégories cartésiennes fermées :

https://mathesismessianisme.wordpress.com/2015/08/28/ccc-cartesian-closed-category-categories-cartesiennes-fermees/

https://hottandphilosophy.wordpress.com/2017/11/18/univalence-in-locally-cartesian-closed-categories/

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/06/chris-kapulkin-type-theory-and-locally-cartesian-closed/

La notion de type dépendant aboutit à la notion de contexte d’un théorème, ou d’une affirmation, c’est à dire une liste de noms de variables , de termes dans un type

Les tribus de Joyal (tribes) sont étroitement associées aux « comprehension categories » :

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/15/hott-relation-des-tribes-et-des-comprehension-categories/

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/15/categorical-models-of-dependent-types/

Une expression x:A est dite contexte d’un jugement :

x:A ⊢ B(x): Type

Voir Page 9 de

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

Les contextes sont introduits à partir de la page 6 dans

http://www.cs.nott.ac.uk/~psxpc2/report-2013.pdf

Ils forment une catégorie (hypothèse naturelle). Un objet terminal de cette catégorie est appelé contexte vide, ce qui correspond au cas où il n’y…

Voir l’article original 528 mots de plus

Publicités