[Agda] Why is propositional equality "Set a" instead of just Set?
Nils Anders Danielsson
nad at cse.gu.se
Thu Aug 22 13:44:06 CEST 2013
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.
--
/NAD
More information about the Agda
mailing list