27 citations · 102 across the 13 of their papers we have counts for
3 papers · 1 filter
Modal Dependent Type Theory and Dependent Right Adjoints
Lars Birkedal, Ranald Clouston, Bassel Mannaa +3
In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked typ…
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…