Avoid universe bumps of `gset`/`mapset` (fixes #134)

I don't understand universes well enough to see why the previous version does not work. So if anyone can explain that, that would be great :).

mentioned in issue #134 (closed)

added 1 commit

• 72adee4c - Some documentation about `mapset`.

Compare with previous version

added 3 commits

• 38d04e99 - Add tests for universe bumping of `gset`.
• 9453a8b5 - CHANGELOG.
• 7baccddd - Some documentation about `mapset`.

Compare with previous version

From comparison: Before this MR:

gset = 
λ (K : Type@{gset.u0}) (EqDecision0 : EqDecision K) (H : Countable K), mapset (gmap K)
     : ∀ (K : Type@{gset.u0}) (EqDecision0 : EqDecision K), Countable K → Type@{max(Set,gmap.u1)}

After this MR:

gset = 
λ (K : Type@{gset.u0}) (EqDecision0 : EqDecision K) (H : Countable K), mapset (gmap K)
     : ∀ (K : Type@{gset.u0}) (EqDecision0 : EqDecision K), Countable K → Set

Otherwise, LGTM -- but I am puzzled why this works.^^

resolved all threads

added 1 commit

• 1a421790 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

I think I developed a little better sense why the previous approach does not work.

Types like gmap Z have type Type@{u} → Type@{u} for any u, i.e., the map is at the same universe as the elements. Hence, gmap Z () would be Set.

However, given mapset : (Type -> Type) -> Type, how could you put universe annotations to make sure that mapset (gmap K) will have type Set? I suppose something like mapset : (M : forall u, Type@{u} → Type@{u}) → Set might work, since M is applied to (), but such higher-ranked types cannot be expressed.

With this MR we have mapset' : Type@{u} → Type@{u}, so then mapset' (gmap K ()) will have type Set.

resolved all threads

merged

mentioned in commit d5b53680

merging.