What a huge loss :(

I have been dreaming that one day we will have a fully developed type system for programming languages based on HoTT and I can develop a new language based on that.