[Agda] Why is propositional equality "Set a" instead of just Set?

Jonathan Leivent jleivent at comcast.net
Sat Aug 17 22:52:02 CEST 2013

Propositional equality is defined in the standard library as:

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

Why isn't it just:

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

The same question applies to many other "proof term" types.

-- Jonathan Leivent

More information about the Agda mailing list