[Agda] Why is propositional equality "Set a" instead of just Set?
Nils Anders Danielsson
nad at cse.gu.se
Fri Aug 23 10:40:39 CEST 2013
On 2013-08-22 15:22, Nils Anders Danielsson wrote:
> However, I guess that we could add another flag:
> --ignore-size-of-indices.
Or perhaps a pragma that attaches to individual mutual blocks.
I've now switched to the following definition:
data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set ℓ where
refl : x ≅ x
--
/NAD
More information about the Agda
mailing list