Meaning of $\mu t$ terms in dependent type theory What is the meaning of the term $\mu t$ in the type theory formalized in this paper (section 2.1, page 2)?
The term μ t is the application of a closure μ to a term t. Similar to how t t' is the application of a term t to t'.