# HITs-Coq Needed: https://github.com/HoTT/HoTT In the pdf more can be found on HITs and the work.