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.