Modeling Martin Löf Type Theory in Categories

François Lamarche 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We present a model of Martin-Lof type theory that includes both dependent products and the identity type. It is based on the category of small categories, with cloven Grothendieck bifibrations used to model dependent types. The identity type is modeled by a path functor that seems to have independent interest from the point of view of homotopy theory. We briefly describe this model's strengths and limitations.
Type de document :
Article dans une revue
Journal of Applied Logic, Elsevier, 2014, 12 (1), pp.28-44. 〈10.1016/j.jal.2013.08.003〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00706562
Contributeur : Francois Lamarche <>
Soumis le : jeudi 19 septembre 2013 - 10:58:31
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : jeudi 6 avril 2017 - 23:46:19

Fichier

IdentityTypesElsev.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

François Lamarche. Modeling Martin Löf Type Theory in Categories. Journal of Applied Logic, Elsevier, 2014, 12 (1), pp.28-44. 〈10.1016/j.jal.2013.08.003〉. 〈hal-00706562v4〉

Partager

Métriques

Consultations de la notice

278

Téléchargements de fichiers

157