Chapter 2 in the Agda proof assistant

I've decided this morning to learn a bit of Agda.
Here's what I've done today, it goes through chapter 2 proving everything in Agda by staying as close as possible to the book (for example when multiple proof terms worked, I choose the one from the book).

I also choose to stay away from implicit propositional equality, with its powerful refl induction. The reason for this is that it looks like Agda is doing all the work and in the end, I still don't understand why things work.

Here is the agda file. It is self-contained but I've stopped at 2.4.7.

IdentityTypes.agda