Decomposing the Univalence Axiom. - Ian Orton; Andrew M. Pitts (TYPES, 2017)

Internal Universes in Models of Homotopy Type Theory. - Daniel R. Licata; Ian Orton; Andrew M. Pitts; Bas Spitters (FSCD, 2018)

Axioms for Modelling Cubical Type Theory in a Topos. - Ian Orton; Andrew M. Pitts (Log. Methods Comput. Sci., 2018)

Models of Type Theory Based on Moore Paths. - Ian Orton; Andrew M. Pitts (Log. Methods Comput. Sci., 2019)

Cubical models of homotopy type theory: an internal approach. - Ian Orton (2019)