  Guarded recursion is a powerful modal approach to recursion that can be seen
as an abstract form of step-indexing. It is currently used extensively in
separation logic to model programming languages with advanced features by
solving domain equations also with negative occurrences. In its multi-clocked
version, guarded recursion can also be used to program with and reason about
coinductive types, encoding the productivity condition required for recursive
definitions in types.
  This paper presents the first denotational model of a type theory combining
multi-clocked guarded recursion with the features of Cubical Type Theory. Using
the combination of Higher Inductive Types (HITs) and guarded recursion allows
for simple programming and reasoning about coinductive types that are
traditionally hard to represent in type theory, such as the type of finitely
branching labelled transition systems. For example, our results imply that
bisimilarity for these imply path equality, and so proofs can be transported
along bisimilarity proofs.
