[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Stefan Monnier]

Andreas Abel writes:
> I think the BUILTIN EQUALITY should be relaxed to allow your definition, and
> also a non-universe-polymorphic one (which some years ago was possible).

If by "your definition" you mean

    data _≡_ {a} {A : Set a} (x : A) : A → Set₀
    where refl : x ≡ x

then it seems to be incompatible with univalence, at least IIUC what
https://github.com/vladimirias/Foundations/blob/master/Coq_patches/README says.

Not sure what you mean by "a non-universe-polymorphic one".

Thorsten Altenkirch writes:
> At least in the case of equality this can be justified by the HoTT
> definition of equality between types at level n to be equivalent to
> equivalence (i.e. there exists a function which is an equivalence) which
> is at the same level.

But, IIUC this justifies an equality such as:

    data _≡_ {a} (x : Set a) : Set a → Set a
    where refl : x ≡ x

i.e. when the equality is between *types*, but not a more general one like

    data _≡_ {a} {A : Set a} (x : A) : A → Set₀
    where refl : x ≡ x

This said, I'm really not knowledgeable about this, I'm just trying to
figure out which rules are valid (and when).  So I'm pointing these
things out to try and get you to tell me what is right ;-)


        Stefan