To fix agda/agda#6654, we've decided that large indices will no longer
be allowed by default. There is an infective flag `--large-indices` to
bring them back, but none of the uses of large indices in the standard
library were essential: to avoid complicated mutually-recursive PRs
across repos, I adjusted the levels to check with `--no-large-indices`
instead of adding the flag to the modules that used them.

bump to 1.7.3 in
- standard-library.agda-lib
- README.agda
- installation-guide.txt

Some objects will get a new name in v2.0.
We add some of these names already here to ease the transition to v2.0:

- add modules `Effect.*` reexporting `Category.*`
- add `IO.Primitive.pure` as alias for `IO.Primitive.return`