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
1 vote
1 answer
38 views

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 testing_factorial.ml file which defines the ...
8 votes
1 answer
117 views

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 ...