Denotational semantics for guarded dependent type theory

摘要

We present a new model of guarded dependent type theory (GDTT), a type theory with guarded recursionand multiple clocks in which one can program with and reason about coinductive types. Productivity ofrecursively defined coinductive programs and proofs is encoded in types using guarded recursion and cantherefore be checked modularly, unlike the syntactic checks implemented in modern proof assistants. Themodel is based on a category of covariant presheaves over a category of time objects, and quantificationover clocks is modelled using a presheaf of clocks. To model the clock irrelevance axiom, crucial for programmingwith coinductive types, types must be interpreted as presheaves internally right orthogonal tothe object of clocks. In the case of dependent types, this translates to a lifting condition similar to the onefound in homotopy theoreticmodels of type theory, but here with an additional requirement of uniquenessof lifts. Since the universes defined by the standard Hofmann–Streicher construction in this model do notsatisfy this property, the universes in GDTT must be indexed by contexts of clock variables. We show howto model these universes in such a way that inclusions of clock contexts give rise to inclusions of universescommuting with type operations on the nose.