Generalize to indexed M-types.
Make definition of M level-polymorphic.
Move M and W types to a common directory.
Refactor W types.

Use implicit arguments like for M types.
Prove that W types are initial algebras.
Add structural equality for W types.
Refactor proof that h-levels are closed under W-types.
Refactor definition of containers.
Add bisimilarity predicate.
Add proof that M-types preserve contractibility.
Finish proof of coinductive extensionality.
Move bisimilarity module into m.
Define well-behaved coinductive extensionality.
add come helper functions for injections
Formatting.