Search Results

Documents authored by Orton, Ian

Document
DOI: 10.4230/LIPIcs.TYPES.2017.6
Decomposing the Univalence Axiom

Authors: Ian Orton and Andrew M. Pitts

Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)

Abstract
This paper investigates Voevodsky's univalence axiom in intensional Martin-Löf type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various published and unpublished sources; we then present a new decomposition of the univalence axiom into simpler axioms. We argue that these axioms are easier to verify in certain potential models of univalent type theory, particularly those models based on cubical sets. Finally we show how this decomposition is relevant to an open problem in type theory.
Cite as

Ian Orton and Andrew M. Pitts. Decomposing the Univalence Axiom. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{orton_et_al:LIPIcs.TYPES.2017.6,
  author =	{Orton, Ian and Pitts, Andrew M.},
  title =	{{Decomposing the Univalence Axiom}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.6},
  URN =		{urn:nbn:de:0030-drops-100546},
  doi =		{10.4230/LIPIcs.TYPES.2017.6},
  annote =	{Keywords: dependent type theory, homotopy type theory, univalent type theory, univalence, cubical type theory, cubical sets}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.22
Internal Universes in Models of Homotopy Type Theory

Authors: Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these model are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-Mörtberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of homotopy type theory within what we call crisp type theory.
Cite as

Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{licata_et_al:LIPIcs.FSCD.2018.22,
  author =	{Licata, Daniel R. and Orton, Ian and Pitts, Andrew M. and Spitters, Bas},
  title =	{{Internal Universes in Models of Homotopy Type Theory}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.22},
  URN =		{urn:nbn:de:0030-drops-91929},
  doi =		{10.4230/LIPIcs.FSCD.2018.22},
  annote =	{Keywords: cubical sets, dependent type theory, homotopy type theory, internal language, modalities, univalent foundations, universes}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.28
Models of Type Theory Based on Moore Paths

Authors: Ian Orton and Andrew M. Pitts

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
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 on cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.
Cite as

Ian Orton and Andrew M. Pitts. Models of Type Theory Based on Moore Paths. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{orton_et_al:LIPIcs.FSCD.2017.28,
  author =	{Orton, Ian and Pitts, Andrew M.},
  title =	{{Models of Type Theory Based on Moore Paths}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{28:1--28:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.28},
  URN =		{urn:nbn:de:0030-drops-77149},
  doi =		{10.4230/LIPIcs.FSCD.2017.28},
  annote =	{Keywords: dependent type theory, homotopy theory, Moore path, topos}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.24
Axioms for Modelling Cubical Type Theory in a Topos

Authors: Ian Orton and Andrew M. Pitts

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an interval-like object I in a topos to give a model of type theory in which elements of identity types are functions with domain I. Cohen, Coquand, Huber and Mörtberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. Furthermore, since our axioms can be satisfied in a number of different ways, we show that there is a range of topos-theoretic models of homotopy type theory in this style.
Cite as

Ian Orton and Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{orton_et_al:LIPIcs.CSL.2016.24,
  author =	{Orton, Ian and Pitts, Andrew M.},
  title =	{{Axioms for Modelling Cubical Type Theory in a Topos}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.24},
  URN =		{urn:nbn:de:0030-drops-65647},
  doi =		{10.4230/LIPIcs.CSL.2016.24},
  annote =	{Keywords: models of dependent type theory, homotopy type theory, cubical sets, cubical type theory, topos, univalence}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact