During a seminar, in which we read and discuss the HoTT book, we got into a heavy battle when trying to guess types in some theorem regarding dependent pairs (likely a generalization of theorem 2.6.5). This was too much for me to bear, so I decided to formalize some HoTT in Coq for educational purposes, starting from scratch (without anything from the standard library, not even the notation for "->").

Update: after battling with formal and informal HoTT for some time, I must say I like it a lot.