Skip to Main content Skip to Navigation
Journal articles

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
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-00706562
Contributor : Francois Lamarche <>
Submitted on : Thursday, September 19, 2013 - 10:58:31 AM
Last modification on : Friday, April 2, 2021 - 8:38:05 AM
Long-term archiving on: : Thursday, April 6, 2017 - 11:46:19 PM

File

IdentityTypesElsev.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

465

Files downloads

704