27 citations · 48 across the 4 of their papers we have counts for
4 papers
Models of Type Theory Based on Moore Paths
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 noti…
Internal Universes in Models of Homotopy Type Theory
Daniel R. Licata, Ian Orton, Andrew M. Pitts +1
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 u…
Decomposing the Univalence Axiom
Ian Orton, Andrew M. Pitts
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 p…
Axioms for Modelling Cubical Type Theory in a Topos
Ian Orton, Andrew M. Pitts
The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object in a topos to give such a path-based model of ty…