@theruran @a_breakin_glass @chjara you can definitely use this to prove things, though, that's very important! especially wrt my distributed-systems goals, since I want to have arbitrary user-defined PORDTs that have guaranteed consistency through embedded proofs (among tons of other things)i don't know exactly what like the class of provable things is, but it's definitely a lot of them. should be equivalent to like non-cubical Agda or something