Intensional type theory with guarded recursive types qua fixed points on universes

Guarded recursive functions and types are useful
for giving semantics to advanced programming languages and
for higher-order programming with infinite data types, such
as streams, e.g., for modeling reactive systems.

We propose an extension of intensional type theory with
rules for forming fixed points of guarded recursive functions.
Guarded recursive types can be formed simply by taking fixed
points of guarded recursive functions on the universe of types.

Moreover, we present a general model construction for
constructing models of the intensional type theory with guarded
recursive functions and types. When applied to the groupoid
model of intensional type theory with the universe of small
discrete groupoids, the construction gives a model of guarded
recursion for which there is a one-to-one correspondence
between fixed points of functions on the universe of types and
fixed points of (suitable) operators on types.

In particular, we find that the functor category
from the preordered set of natural numbers to the category of
groupoids is a model of intensional type theory with guarded
recursive types.