notation that does nothing

Stream: general

[Johan Commelin]

I want something like this:

local notation ` [`n`] ` := (((id : ℕ → simplex_category) (n)) : simplex_category)
instance : has_coe_to_sort simplex_category := { S := Type, coe := λ n, fin $ n+1 }

In other words, it should take whatever is between [ and ], interpret that as a ℕ, but interpret [_] as an element of simplex_category.
In this way, I can talk about [n+1] without defining addition or one for simplex_category. In this way I can also coerce [n] to fin (n+1) without defining that coercion for all naturals.
In other words, I would like to make sure that i : [n+1] typechecks.

[Simon Hudon]

Your snippet doesn't work?

[Chris Hughes]

Isn't this overloaded from list

[Chris Hughes]

Use a different type of brackets?

[Simon Hudon]

Instead of using id, try using:

def my_brackets (n : nat) : simplex_category := n
local notation ` [`n`] ` := my_brackets n

[Simon Hudon]

Yes, that's also true

[Simon Hudon]

A lot of brackets are already taken

[Johan Commelin]

I now have

inductive simplex_category
| from_nat : ℕ → simplex_category

namespace simplex_category

local notation ` [`n`] ` := from_nat n

instance : has_coe_to_sort simplex_category :=
{ S := Type,
  coe := λ n, simplex_category.cases_on n (λ n, fin $ n+1) }

instance {Δ : simplex_category} : linear_order Δ := by cases Δ; unfold_coes; apply_instance

instance : category_theory.category simplex_category :=
{ hom := λ Δ Δ', {f : Δ → Δ' // monotone f},
  id := λ _, ⟨_, monotone_id⟩,
  comp := λ _ _ _ f g, ⟨_, monotone_comp f.2 g.2⟩ }

It seems to work as intended. It seems like a bit of a trick to define and inductive type that is equivalent to nat, but whatever.

[Johan Commelin]

And I definitely want [n] notation. It's just silly that the notation for lists isn't local.

[Kevin Buzzard]

Making copies of inductive types is not uncommon. If you want to do congruence mod n on the integers, you run into problems because equivalence relations are a class but you want more than one equivalence relation on the integers. You can fix it by making these fake copies.