@Andrev I like it but I'm not a cubical person generally so I would also like something like Agda but for good old-fashioned ITT. Maybe this is a sign I should actually learn Idris properly.
@liamoc Idris2 is still not ready; Idris1 is not under active development. I am worried about the risk of being obsolete soon if doing works with Idris
