[Agda] Why is propositional equality "Set a" instead of just Set?
Jonathan Leivent
jleivent at comcast.net
Thu Aug 22 17:00:27 CEST 2013
On 08/22/2013 07:44 AM, Nils Anders Danielsson wrote:
> On 2013-08-21 22:29, Jonathan Leivent wrote:
>> Hetero equality is at level zero (in standard library 0.7):
>>
>> -- Heterogeneous equality
>>
>> infix 4 _≅_
>>
>> data _≅_ {a} {A : Set a} (x : A) : ∀ {b} {B : Set b} → B → Set where
>> refl : x ≅ x
>>
>> I guess this can't be correct - or, at least, isn't consistent with
>> where type theory is headed these days.
>
> Heterogeneous equality isn't very useful when --without-K is used.
> Furthermore it's not quite clear to me how the definition should be
> changed. The following, less universe-polymorphic definition seems
> reasonable to me:
>
> data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set (suc ℓ) where
> refl : x ≅ x
>
> If others agree, then I can switch to this definition.
>
Just to be clear, do you intend the "suc" only for hetero equality, not
normal prop equality? So, normal prop equality would stay at its
current level (Set ℓ), but hetero equality would be one level above?
-- Jonathan
More information about the Agda
mailing list