M types

Stream: mathlib4

[Violeta Hernández]

I'm currently trying to wrap my head around M-types in type theory. I've been having a bit of a hard time reading through https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/PFunctor/Univariate/M.html, since it seems like a large amount of the file is dedicated to setting up the type and proving its universal properties, which to me seem like they should be private material.

[Violeta Hernández]

Surely everything about Approx can be made private? To me it seems like it's just an implementation detail, though I might be wrong.