# Zulip Chat Archive

## Stream: general

### Topic: notation that does nothing

#### Johan Commelin (Nov 21 2018 at 12:42):

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 (Nov 21 2018 at 20:21):

Your snippet doesn't work?

#### Chris Hughes (Nov 21 2018 at 20:23):

Isn't this overloaded from `list`

#### Chris Hughes (Nov 21 2018 at 20:23):

Use a different type of brackets?

#### Simon Hudon (Nov 21 2018 at 20:23):

Instead of using `id`

, try using:

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

#### Simon Hudon (Nov 21 2018 at 20:24):

Yes, that's also true

#### Simon Hudon (Nov 21 2018 at 20:24):

A lot of brackets are already taken

#### Johan Commelin (Nov 21 2018 at 20:37):

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 (Nov 21 2018 at 20:38):

And I definitely want `[n]`

notation. It's just silly that the notation for lists isn't local.

#### Kevin Buzzard (Nov 21 2018 at 20:50):

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.

Last updated: May 13 2021 at 16:25 UTC