Zulip Chat Archive

Stream: general

Topic: has_mem notation


view this post on Zulip Johan Commelin (Jan 14 2019 at 10:46):

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)

view this post on Zulip Johan Commelin (Jan 14 2019 at 10:46):

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

view this post on Zulip Chris Hughes (Jan 14 2019 at 10:49):

Could you do a has_mem instance instead?

view this post on Zulip Johan Commelin (Jan 14 2019 at 11:28):

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.


Last updated: May 13 2021 at 22:15 UTC