  Clocked Cubical Type Theory is a new type theory combining the power of
guarded recursion with univalence and higher inductive types (HITs). This type
theory can be used as a metalanguage for synthetic guarded domain theory in
which one can solve guarded recursive type equations, also with negative
variable occurrences, and use these to construct models for reasoning about
programming languages. Combining this with HITs allows for the use of type
constructors familiar from set-theory based approaches to semantics, such as
quotients and finite powersets in these models.
  In this paper we show how to reason about the combination of finite
non-determinism and recursion in this type theory. Unlike traditional domain
theory which takes an ordering of programs as primitive, synthetic guarded
domain theory takes the notion of computation step as primitive in the form of
a modal operator. We use this extra intensional information to define two
guarded recursive (finite) powerdomain constructions differing in the way
non-determinism interacts with the computation steps. As an example application
of these we show how to prove applicative similarity a congruence in the cases
of may- and must-convergence for the untyped lambda calculus with finite
non-determinism. Such results are usually proved using operational reasoning
and Howe's method. Here we use an adaptation of a denotational method developed
by Pitts in the context of domain theory.
