| Axioms for modelling cubical type theory in a topos I Orton, AM Pitts Logical Methods in Computer Science 14, 2018 | 120 | 2018 |
| Internal universes in models of homotopy type theory DR Licata, I Orton, AM Pitts, B Spitters arXiv preprint arXiv:1801.07664, 2018 | 95 | 2018 |
| Decomposing the univalence axiom I Orton, AM Pitts arXiv preprint arXiv:1712.04890, 2017 | 8 | 2017 |
| Cubical Models of Homotopy Type Theory-An Internal Approach RI Orton | 4 | 2019 |
| Models of type theory based on Moore paths I Orton, AM Pitts Logical Methods in Computer Science 15 (Type theory and constructive …, 2019 | 3 | 2019 |
| Agda code accompanying PhD thesis: Cubical Models of Homotopy Type Theory--An Internal Approach R Orton | 2 | 2019 |
| Code supporting Axioms for Modelling Cubical Type Theory in a Topos I Orton, A Pitts | 2 | 2018 |
| Internal Universes in Models of Homotopy Type Theory AM Pitts, D Licata, I Orton, B Spitters Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 2018 | | 2018 |
| Code supporting Decomposing the Univalence Axiom RI Orton, A Pitts | | 2018 |
| Code supporting Internal Universes in Models of Homotopy Type Theory AM Pitts, I Orton, DR Licata, B Spitters | | 2018 |
| 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) M Gaboardi, G Moser, A Silva, C Tasson, B Ahrens, PLF Lumsdaine, ... Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, 2017 | | 2017 |
| Denotational semantics Exercises O Kammar, I Orton | | 2015 |
| Axioms for univalence I Orton, A Pitts | | |
