8
$\begingroup$

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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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 $\endgroup$
    – Joey Eremondi
    Mar 4, 2022 at 22:33
  • 2
    $\begingroup$ 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... $\endgroup$
    – Jonathan Sterling
    Mar 7, 2022 at 10:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.