Modeling Martin Löf Type Theory in Categories - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Applied Logic Année : 2014

Modeling Martin Löf Type Theory in Categories

Résumé

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.
Fichier principal
Vignette du fichier
IdentityTypesElsev.pdf (404.99 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00706562 , version 1 (11-06-2012)
hal-00706562 , version 2 (18-12-2012)
hal-00706562 , version 3 (30-08-2013)
hal-00706562 , version 4 (19-09-2013)

Identifiants

Citer

François Lamarche. Modeling Martin Löf Type Theory in Categories. Journal of Applied Logic, 2014, 12 (1), pp.28-44. ⟨10.1016/j.jal.2013.08.003⟩. ⟨hal-00706562v4⟩
324 Consultations
375 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More