# Are P x and ▸ ((next P) ⊛ (next x)) equivalent in Guarded Cubical Agda?

In Guarded Cubical Agda there's ▹_ : Set i → Set i  and ▸_ : ▹ Set i → Set i.

If I've got P : X -> Set and x : X, are P x and ▸ ((next P) ⊛ (next x)) equivalent? If so, can it be proved internally or only as a metatheorem? Are there different guarded type theory implementations (Iris, maybe) that would support this?

My thought is that once you know that x is the result of next and not some fixed-point computation, then the only way to inhabit ▸ ((next P) ⊛ (next x)) is to have a P x lifted into it using next. I'm still wrapping my head around this guarded stuff, so I might be misunderstanding.

These are not equivalent; ▸ ((next P) ⊛ (next x)) is equivalent to ▹ (P x). Hence if it were equivalent to (P x), we would have that ▹ X is equivalent to X for all X : Set. The purpose of the filled in modality (which I think of as the "dependent modality") is to apply the later modality to a type that only exists later; in conjunction with the "tick syntax" of Guarded Cubical Agda, this provides a more easily implemented alternative to the delayed substitution syntax of Guarded Dependent Type Theory from the old days.
• Thanks, that's helpful. So to check, you use ▸ when constructing a non-positive datatype, so that you can transform the ▹ Set that fix gives you into a Set, right? Is there a way to express the idea of "I have x : ▹ X, and a proof that if x terminates (i.e. is equal to next y for some y) then P y holds? I'm essentially trying to prove something up-to termination Mar 4, 2022 at 22:33
• You can write down such a thing, but I would clarify that "later A" should not be thought of as "an element of A that might not terminate" --- though such a notion can be formalized in terms of the later modality. What you want is the "guarded lift monad", which is the guarded-recursive type given by two constructors: now : A -> Lift(A) and step : later(Lift(A)) -> Lift(A). It is worth having a glance at Marco Paviotti's thesis to see what you might do with such a type... Mar 7, 2022 at 10:03