Denotational semantics for guarded dependent type theory

TL;DR

This paper introduces a new denotational semantics model for Guarded Dependent Type Theory (GDTT), enabling modular verification of productivity in coinductive types using categorical presheaves and clock quantification.

Contribution

It provides a novel categorical model for GDTT that captures guarded recursion and clock irrelevance, addressing limitations of syntactic checks in proof assistants.

Findings

Model based on covariant presheaves over time objects

Handles clock irrelevance via presheaves orthogonal to clock objects

Universes indexed by clock contexts with inclusion-preserving properties

Abstract

We present a new model of Guarded Dependent Type Theory (GDTT), a type theory with guarded recursion and multiple clocks in which one can program with, and reason about coinductive types. Productivity of recursively defined coinductive programs and proofs is encoded in types using guarded recursion, and can therefore be checked modularly, unlike the syntactic checks implemented in modern proof assistants. The model is based on a category of covariant presheaves over a category of time objects, and quantification over clocks is modelled using a presheaf of clocks. To model the clock irrelevance axiom, crucial for programming with coinductive types, types must be interpreted as presheaves orthogonal to the object of clocks. In the case of dependent types, this translates to a lifting condition similar to the one found in homotopy theoretic models of type theory, but here with an additional requirement of uniqueness of lifts. Since the universes defined by the standard Hofmann-Streicher construction in this model do not satisfy this property, the universes in GDTT must be indexed by contexts of clock variables. We show how to model these universes in such a way that inclusions of clock contexts give rise to inclusions of universes commuting with type operations on the nose.