You are a computer scientist, not a mathematician. This book is for mathematicians. (Not an insult, the mathematicians deep into homotopy aren't likely to be gr

You are a computer scientist, not a mathematician. This book is for mathematicians. (Not an insult, the mathematicians deep into homotopy aren't likely to be great at building an actual theorem prover on a computer.) Basic notions of topology only touch a bit of the corners of HoTT. Have you seen the Agda code on the HoTT github site? That might be closer to your language. Or poke around at Andrej Bauer's work, as he leans toward the computerization side a bit.