I wonder if it somehow can be integrated with Coq[1] and Univalent Foundations[2]. Probably these can be used as a more substantial "base" for this machine. [1

I wonder if it somehow can be integrated with Coq[1] and Univalent Foundations[2]. Probably these can be used as a more substantial "base" for this machine. [1] https://github.com/coq/coq https://github.com/coq/coq [2] https://github.com/UniMath https://github.com/UniMath