How to redefine standard notation?

Stream: new members

[Ignat Insarov]

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]

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

[Riccardo Brasca]

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]

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

[Johan Commelin]

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

[Ignat Insarov]

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]

How do I spell that in Lean?

[Mario Carneiro]

Yeah, lean 3 doesn't really support this

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Ignat Insarov]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

it's mostly intended for writing the core library itself

[Ignat Insarov]

Yes, I should have to live with that.

[Mario Carneiro]

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]

Yes, local notation works too.

[Ignat Insarov]

Lean is a nice language.

[Ignat Insarov]

It lets me do things.