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