Archives pour la catégorie topos theory

Laurent Lafforgue : l’importance des topoi de Grothendieck

youtu.be/Wmhwaso_b3M

Badiou : métaphysique du multiple

http://jef-safi.net/spip/spip.php?article231

Olivia Caramello introduction à son livre « Theories, sites, toposes

#HoTT André Joyal extension et restriction de contexte

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

http://www1.maths.leeds.ac.uk/~pmtng/HOMALG/joyal-mit.pdf

Un type est un objet E d’une tribu C, c’est à dire une catégorie satisfaisant certaines conditions cf page 13 sur 81:

⊢E : Type

Un terme est un élément d’un type E, c’est à dire catégoriquement un morphisme de l’objet terminal de la tribu vers l’objet E

Page 22 sur 81

A est un objet d’une tribu C c’est à dire un type

On considère le foncteur changement de base ( foncteur de substitution) le long du morphisme unique de A vers l’objet terminal de la tribu :

A ? *

iA : C ? C(A)

C’est un homomorphisme de tribus ( voir Page 21 sur 81)

Par définition : iA( E)= ( ExA, p2)

(Voir Page 12 sur 81)

Ce foncteur correspond en théorie des types à une régle de déduction appelée affaiblissement contextuel , qui consiste à déduire :

x:A ⊢E:…

Voir l’article original 259 mots de plus