| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 4662955 | Journal of Applied Logic | 2014 | 17 Pages |
Abstract
We present a model of Martin-Löf 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.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
François Lamarche,