nLab Ian Orton

• GoogleScholar page

Selected writings

On categorical semantics for Martin-Loef type theory:

• Ian Orton, Andrew M. Pitts, Models of Type Theory Based on Moore Paths, Logical Methods in Computer Science 15 1 (2019) 2:1–2:24 [arXiv:1802.05629, doi:10.23638/LMCS-15(1:2)2019]

On type universes in homotopy type theory:

• Daniel R. Licata, Ian Orton, Andrew M. Pitts, 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) 108 (2018) 22:1–22:17 [arXiv:1801.07664, doi:10.4230/LIPIcs.FSCD.2018.22]

On cubical type theory:

• Ian Orton, Andrew M. Pitts, Axioms for Modelling Cubical Type Theory in a Topos, Logical Methods in Computer Science 14 4 (2018) 1–33 [arXiv:1712.04864, doi:10.23638/LMCS-14(4:23)2018]

On the univalence axiom:

• Ian Orton, 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) 104 (2019) 6:1–6:19 [arXiv:1712.04890, doi:10.4230/LIPIcs.TYPES.2017.6]

category: people