Skip to main content
5 votes
Accepted

Are `P x` and `▸ ((next P) ⊛ (next x))` equivalent in Guarded Cubical Agda?

These are not equivalent; ▸ ((next P) ⊛ (next x)) is equivalent to ▹ (P x). Hence if it were equivalent to ...
Jonathan Sterling's user avatar
3 votes
Accepted

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

I found my answer in Guarded Domain Theory and its implementation in Guarded Cubical Agda (implementing Ticked Cubical Type Theory). The following program type-checks ...
Sebastian Graf's user avatar
2 votes

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

The easiest thing to do seems to be to disable termination checking. There is a setting in coq-of-ocaml to insert Unset Guard Checking in the generated file. Of ...
Li-yao Xia's user avatar
  • 1,857
1 vote

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

Your datatype is a variant of the domain equation for the untyped lambda calculus. Verifying that an arbitrary untyped lambda term is normalizing is an undecidable problem, but there are undecidable ...
Max New's user avatar
  • 314

Only top scored, non community-wiki answers of a minimum length are eligible