Simpler proof of naturality square

[PHart3]

1. This pull request reduces the complexity of the proof of the pre-composition naturality square, contained in the Map-Nat folder.

• The main point is that it now shows that the map induced by a map of spans equals the canonical map by showing that both are in the same fiber of the post-composition equivalence.
• This results in fewer long computations than those involved in the original proof.

2. It also does a good amount of clean-up and rearranging across the entire code base.
3. One notable change to the Dockerfile is installing happy-lib-2.0.2 instead of the latest version of Happy. It seems that the latter breaks the parser of Agda 2.6.3.

[favonia]

@PHart3 Thinking about it, if v1-install will work with a fixed version of happy, maybe it's better to also change v2-install back to v1-install.

[PHart3]

@PHart3 Thinking about it, if v1-install will work with a fixed version of happy, maybe it's better to also change v2-install back to v1-install.

@favonia It does not work with happy-2.0.2. It generates a different error, an interface file error. See here.