1
Formalizowanie teorii typów homotopii w Idris
Patrząc na blog dotyczący teorii homotopii, łatwo można znaleźć wiele bibliotek formalizujących większość teorii typów homotopii w Agdzie i Coq. Czy ktoś wie, czy istnieje podobna próba sformalizowania HoTT w Idris ?