[gylterud]

Agda is a nice language with a good homotopy type theory library based on the univalence axiom called agda-unimath.