[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Andreas Abel]

On 06.01.2017 22:29, Stefan Monnier wrote:
> 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.

Ok, but this is independent of whether it can be a BUILTIN or not.

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

Of type

   {A : Set} (x y : A) -> Set

See also issue #2386: https://github.com/agda/agda/issues/2386

> 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.

At the same level means "at level n"?

>
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/