1: \begin{abstract} 

2: Clocked Cubical Type Theory is a new type theory combining the power of guarded

3: recursion with univalence and higher inductive types (HITs). This type theory

4: can be used as a metalanguage for \emph{synthetic guarded domain theory} in which one 

5: can solve guarded recursive type equations, also with negative variable occurrences,

6: and use these to construct models for reasoning about programming languages. 

7: Combining this with HITs allows for the use of type constructors familiar from set-theory 

8: based approaches to semantics, such as quotients and finite powersets in these models.

9: 

10: In this paper we show how to reason about the combination of finite non-determinism and 

11: recursion in this type theory. Unlike traditional domain theory which takes an ordering of programs as

12: primitive, synthetic guarded domain theory takes the notion of computation step as primitive

13: in the form of a modal operator. We use this extra intensional information to define 

14: two guarded recursive (finite) powerdomain constructions differing in the way 

15: non-determinism interacts with the computation steps. As an example application of these

16: we show how to prove applicative similarity a congruence 

17: in the cases of may- and must-convergence for the untyped lambda calculus with finite 

18: non-determinism. Such results are usually proved using operational

19: reasoning and Howe's method. Here we use an adaptation of a denotational method 

20: developed by Pitts in the context of domain theory.

21: \end{abstract}

22: