As argued by @nmvdw in the discussion about [PR 1582 of UniMath](https://github.com/UniMath/UniMath/pull/1582), the inclusion of material from PAdics is not even needed.
As argued by @nmvdw in the discussion about PR 1582 of UniMath, the inclusion of material from PAdics is not even needed.