#HoTT : André Joyal : tribes and fibrations

Donc, récapitulons :

https://ncatlab.org/homotopytypetheory/files/Joyal.pdf

Un type est un objet d’une catégorie, appelée tribu (tribe) munie d’une classe F de morphismes, appelée « tribe Structure » ayant certaines propriétés particulières (page 14 sur 81)
notamment des propriétés de fermeture pour certaines opérations, ainsi que de contenir les isomorphismes.
Une fibration est un morphisme de cette classe F.
On peut choisir les fibrations, à condition qu’elles respectent les propriétés de base.

https://ncatlab.org/nlab/show/fibration

Exemples de tribus :

– Toute catégorie munie de produits finis, si l’on choisit les projections comme fibrations

– La catégorie Grpd des groupoides, si l’on choisit comme fibrations les iso-fibrations

https://ncatlab.org/nlab/show/isofibration
– La catégorie Kan des complexes de Kan si l’on choisit comme fibrations les fibrations de Kan

https://ncatlab.org/nlab/show/Kan+complex

https://en.m.wikipedia.org/wiki/Kan_fibration

– La catégorie des objets fibrants :

https://en.m.wikipedia.org/wiki/Fibrant_object

D’une catégorie modèle de Quillen.

Un terme t de type E:

t:E

Est un morphisme de l’objet terminal de la tribu C (il y en a toujours un dans toute tribu) vers E : c’est un élément généralisé de E .

Page 17 sur 81 :
Une fibration p: E → A

Est une famille d’objets de la tribu C paramétrée (indexée) par un élément variable x de A

{E(x) x ∊ A}

Une tribu est donc une collection de familles fermée pour certaines opérations.

Tribu locale C(A) , A étant un objet d’une tribu C: Page 18 sur 81 de la note de Joyal :

C’est la sous-catégorie de la « slice category » C/A dont les objets (E,p) sont les fibrations p: E → A ayant pour cible A

Ces objets sont les types dépendant de contexte A, ce que l’on note:

x:A ⊢E(x) : Type

Une section t:

https://fr.m.wikipedia.org/wiki/Section_(théorie_des_catégories)

De p: E → A

Est appelé un terme dépendant t(x):E(x)

notation:

x:A ⊢ t(x):E(x)

Voici les liens de documents cités par Joyal, dans sa note :

http://www.crm.cat/en/Activities/Documents/joyal-crm-2013.pdf

(Page 8 sur 75)

https://ncatlab.org/nlab/files/CurienGarnerHofmann.pdf

https://people.mpi-sws.org/~dreyer/courses/catlogic/jacobs.pdf

https://www.dpmms.cam.ac.uk/~martin/Research/Pub71-80/hjp80.pdf

http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf

http://www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf

(Je ne trouve pas en lecture gratuite « Semantics of type theory » de Streicher)

http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/FibLec.pdf

Advertisements
This entry was posted in ∞-catégories, ∞-topoi, category theory, homotopy type theory, Philosophie mathématique, Science-internelle, Théorie des topoi (topos theory). Bookmark the permalink.