[haltist]

It should be possible to embed cubical type theory in Idris.[1][2]

1: https://arxiv.org/abs/2210.08232

2: https://chat.openai.com/share/aadb7a0a-08a4-4951-b877-cb2f61...