ParentFull threadxvilka·Shouldn't it be written with Coq instead? Like UniMath[1] for example?[1] https://github.com/UniMathView on HN