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: Dec 20 2023 at 11:08 UTC