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.