Towards changing things and see if it proofs
A cubical type theory implementation. features you might not found in Coq, Agda, Lean:
see roadmap for details.
see library and tests folder for sample code. for example Brunerie Number