Cubical https://github.com/mortberg/cubicaltt https://github.com/mortberg/cubicaltt is a proof of concept programming language based on constructive (cubical ty

Cubical https://github.com/mortberg/cubicaltt https://github.com/mortberg/cubicaltt is a proof of concept programming language based on constructive (cubical type theory https://arxiv.org/abs/1611.02108 https://arxiv.org/abs/1611.02108) interpretation of HoTT. Agda also added recently support for cubical paths https://agda.readthedocs.io/en/latest/language/cubical.html https://agda.readthedocs.io/en/latest/language/cubical.html . I'm also waiting on Lean https://leanprover.github.io https://leanprover.github.io to introduce cubical type theory for HoTT. Version 2 of the language had HoTT based on the univalence axiom which was dropped in version 3. With cubical type theory the univalence axiom can be constructively proved and is no longer an axiom.