Universal Covers

This upstream file currently contains only commented exploratory code after the FreeGroupoid import, so the Lean Pool port keeps the importable module stub.