Non-portable module names (case-sensitivity)
Hello, I tried to clone your repo on macOS, but it breaks because my filesystem is case-insensitive and thus there is a clash between e.g. html/Universes.md and html/universes.md.
Agda also doesn't play along for me, because your own universes module clashes in Agda with Martin Escardo's Universes module (due to the case-insensitive FS). [As a workaround, I renamed your version to my-universes and then Agda would proceed.]
Future versions of Agda may not allow module names that differ only by case, see discussion at https://github.com/agda/agda/issues/4678.