λ(a : Type) → { eq : a → a → Bool }