Ian Orton ; Andrew M. Pitts - Models of Type Theory Based on Moore Paths

lmcs:4292 - Logical Methods in Computer Science, January 9, 2019, Volume 15, Issue 1 - https://doi.org/10.23638/LMCS-15(1:2)2019
Models of Type Theory Based on Moore PathsArticle

Authors: Ian Orton ; Andrew M. Pitts

    This paper introduces a new family of models of intensional Martin-Löf type theory. We use constructive ordered algebra in toposes. Identity types in the models are given by a notion of Moore path. By considering a particular gros topos, we show that there is such a model that is non-truncated, i.e. contains non-trivial structure at all dimensions. In other words, in this model a type in a nested sequence of identity types can contain more than one element, no matter how great the degree of nesting. Although inspired by existing non-truncated models of type theory based on simplicial and cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.


    Volume: Volume 15, Issue 1
    Section: Type theory and constructive mathematics
    Published on: January 9, 2019
    Accepted on: December 18, 2018
    Submitted on: February 16, 2018
    Keywords: Computer Science - Logic in Computer Science,F.4.1,F.3.2
    Funding:
      Source : OpenAIRE Graph
    • DTA - University of Cambridge; Funder: UK Research and Innovation; Code: EP/L504920/1

    1 Document citing this article

    Consultation statistics

    This page has been seen 1621 times.
    This article's PDF has been downloaded 559 times.