This repo was my first learning project. I barely knew Idris, and have no experience with HoTT. Please don't judge the language referring to this. You can refer

This repo was my first learning project. I barely knew Idris, and have no experience with HoTT. Please don't judge the language referring to this. You can refer nice code here https://github.com/JetBrains/arend-lib https://github.com/JetBrains/arend-lib