Archives pour la catégorie topos theory

Paugam : towards the mathematics of quantum field theory

via F Paugam : towards the mathematics of quantum field theory

Publicités

Biequivalence of LCCC and MLTT

http://perso.ens-lyon.fr/pierre.clairambault/maintlca.pdf

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

Hurewicz fibrations in elementary toposes

https://arxiv.org/pdf/1608.02509.pdf

Les tribus (tribes) de Joyal y sont étudiées , la notion de topos de Hurewicz est définie et on y montre qu’il s’agit d’une tribu (« type theoretical tribe »)