2-coherence of truncation, newer Agda version, etc.

[PHart3]

1. This PR adds a proof of 2-coherence for the $n$-truncation functor on coslices (which confirms that it preserves colimits as a left adjoint to the forgetful functor). The proof is a routine verification.
2. It also updates Docker to run on Agda 2.6.4.3.
3. Finally, it makes a small change to the definition of homotopy of pointed maps by using the normal identity type instead of path-seq. This makes the definition correct with respect to the structure identity principle.