Containers (and W and M)

[stefaniatadama]

This PR adds some definitions and proofs on containers. As a prerequisite, it also required adding (non-indexed) W-types and M-types written as a record type.

More specifically,

• we define the category of generalised containers,
• we define the container extension functor,
• we give two different presentations of the proof that the container extension functor is full and faithful,
• and we give proofs that set-containers are closed under least and greatest fixed points.

Most of the proofs are an adaptation of those in 'Containers: Constructing strictly positive types' by Abbott, Altenkirch, and Ghani.

I am aware of the -W[no]NoGuardednessFlag warning being raised. This warning is raised because MRecord.agda is not tagged with a --guardedness flag. I avoided this tag as I import MRecord.agda from Algebras.agda, which exists in the Data directory, and which therefore causes an error if it is also tagged with --guardedness. I'd be happy to refactor if reviewers have suggestions on how else I can organise things.