Syntax and Models of Cartesian Cubical Type Theory

I'd like to understand this paper enough to know how to implement cubical type theory. However I'm confused about how cofibrations should be implemented. They are a central piece in the paper.

I started an nbe implementation that may help on the way. It handles intervals with de bruijn indices to allow case splitting under them, hopefully I got that correct.

Specifically I wonder what kind of computational behavior cofibrations refer to?

  • 2
    $\begingroup$ Let me shamelessly self-promote this arxiv.org/abs/2210.08232 and you need a union-find data structure to speed up the decision procedure of whether cofibs are true or not $\endgroup$
    – ice1000
    Commented Dec 11, 2023 at 2:38
  • 2
    $\begingroup$ You can check the actual implementation in github.com/RedPRL/kado. If you don’t have diagonals (CHM/CCHM as in the article above, i.e. Cubical Agda/cubicaltt), the problem is about DNF computations, that is, some search tree algorithms; diagonals (as in redtt/cooltt) make things more complicated, but it’s still very similar. $\endgroup$
    – siegment
    Commented Dec 11, 2023 at 8:02
  • $\begingroup$ Do you also have the project that uses kado? I did just take a look at kado and didn't understand how it maps over to the things described in the paper. $\endgroup$
    – Cheery
    Commented Dec 11, 2023 at 9:26
  • 1
    $\begingroup$ There is github.com/RedPRL/cooltt/tree/main/src/core (obviously). $\endgroup$
    – siegment
    Commented Dec 11, 2023 at 9:45


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.