has_mem notation

Stream: general

[Johan Commelin]

Does anyone know how to fix this notation hack?

def covering_family {X : Type u} [category.{v} X] (U : X) : Type (max u v) :=
Π {{V}}, set (V ⟶ U)

local notation a `∈`:50 b:50 := b a -- Aaahrg!

structure coverage (X : Type u) [category.{v} X] :=
(covers   : Π (U : X), set (covering_family U))
(property : ∀ {U V : X} (g : V ⟶ U),
            ∀ f ∈ covers U, ∃ h ∈ covers V,
            ∀ Vj (k : Vj ⟶ V), k ∈ h →
            ∃ Ui (l : Ui ⟶ U), l ∈ f ∧ ∃ m : Vj ⟶ Ui, m ≫ l = k ≫ g)

[Johan Commelin]

Ooh, and here is the relevant top of the file

import category_theory.presheaf
import category_theory.comma
import category_theory.full_subcategory
import analysis.topology.topological_space
import category_theory.examples.topological_spaces
import tactic.where

universes v u

namespace category_theory
open category_theory
open category_theory.limits

[Chris Hughes]

Could you do a has_mem instance instead?

[Johan Commelin]

No, I don't think has_mem works. I want to say that f : V ⟶ U is a member of c. But the type of f depends on V, which ranges over all of X.