Comment by m_j_g

cubical Agda : https://github.com/agda/cubical is also worth mentioning int this context