Zulip Chat Archive

Stream: new members

Topic: How to redefine standard notation?


Ignat Insarov (Oct 04 2021 at 08:43):

I observe that is defined as function.comp : (?M_2 → ?M_3) → (?M_1 → ?M_2) → ?M_1 → ?M_3. I want to define it as a composition in any category. How should I go about it?

Specifically, how can I avoid the standard notation being brought into scope?

Ignat Insarov (Oct 04 2021 at 08:46):

I reckon there is another symbol for composition in the standard for Category Theory but I want to do it my way.

Riccardo Brasca (Oct 04 2021 at 08:55):

There might be a way of doing it, but I think the general principle is to not mess up with things in core. Note that docs#function.comp is not a special case of composition in a category: functions are a primitive notion in type theory, they are not literally morphisms in the category of sets. (Of course there is category of sets with its hom, but these are denoted with a slightly different arrow .)

Ignat Insarov (Oct 04 2021 at 09:01):

Even with these considerations in mind, I still want to have a choice to ignore the standard library.

Johan Commelin (Oct 04 2021 at 09:01):

@Ignat Insarov You can start your file with prelude, and ignore the rest of humanity :crazy:

Ignat Insarov (Oct 04 2021 at 09:02):

For example, in Haskell I can say import Prelude hiding ((.)) and it will hide the standard composition so I can define my own.

Ignat Insarov (Oct 04 2021 at 09:02):

How do I spell that in Lean?

Mario Carneiro (Oct 04 2021 at 09:02):

Yeah, lean 3 doesn't really support this

Mario Carneiro (Oct 04 2021 at 09:03):

everyone has to live with the choices made by core, which puts a high bar on what can be included

Mario Carneiro (Oct 04 2021 at 09:03):

and there are periodically PRs to core lean that remove or modify stuff like this because of issues downstream

Mario Carneiro (Oct 04 2021 at 09:04):

That said, it is possible to make a local notation for your own thing, and it will "win" over the definition in core

Mario Carneiro (Oct 04 2021 at 09:05):

but it's not recommended since this isn't what I would call "being a team player"

Ignat Insarov (Oct 04 2021 at 09:05):

I think I can do the prelude thing mentioned by Riccardo and then tediously import things that I do want, such as Prop.

Mario Carneiro (Oct 04 2021 at 09:06):

The prelude suggestion was facetious. No one would write code like that, not least because you lose any ability to use tactics

Mario Carneiro (Oct 04 2021 at 09:07):

That is, there are certain bootstrapping steps that are needed for lean to function normally, and using prelude skips that

Mario Carneiro (Oct 04 2021 at 09:07):

it's mostly intended for writing the core library itself

Ignat Insarov (Oct 04 2021 at 09:08):

Yes, I should have to live with that.

Mario Carneiro (Oct 04 2021 at 09:09):

But it's not really necessary to literally exclude the definition of function.comp, if you are just trying to make the notation do something else

Ignat Insarov (Oct 04 2021 at 09:09):

Yes, local notation works too.

Ignat Insarov (Oct 04 2021 at 09:09):

Lean is a nice language.

Ignat Insarov (Oct 04 2021 at 09:10):

It lets me do things.


Last updated: Dec 20 2023 at 11:08 UTC