Questions tagged [guarded-recursion]

Cubical Agda is extended with Nakano’s later modality and guarded recursion based on Ticked Cubical Type Theory. (from Agda)

Filter by
Sorted by
Tagged with
6 votes
2 answers

Is there a formalism of "coinductive" data types with negative occurrences?

Consider the following program in Haskell: ...
Sebastian Graf's user avatar
1 vote
1 answer

How do I work with ints when using coq-of-ocaml for OCaml to Coq conversion?

I am trying to use coq-of-ocaml to convert a simple recursive factorial function written in OCaml into Coq. I have a file which defines the ...
bodacious_bandit's user avatar
8 votes
1 answer

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 ...
Joey Eremondi's user avatar