Frankly because I don’t get it and hope that somebody in the comments will say something that helps me to understand.
If HoTT is what you are interested in, I recommend this single-page introduction if you are already familiar with how dependent type theory is used for theorem proving: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes...