Notation in typeclass definitions

Stream: lean4

[Chris Henson]

Is there a way to define a notation at the same time as a typeclass? In Coq I might do something like

Reserved Infix "~>" (at level 90, right associativity).

Class Category : Type := {
  object: Type;
  arrow: object -> object -> Type where "a ~> b" := (arrow a b);
  .
  .
  .
 (* the rest of the typeclass, can now use the ~> notation for readability *)
}

Notation "f ~> g"   := (arrow f g) (at level 90, right associativity)

Is there a Lean equivalent?

[Horațiu Cheval]

I know of a hacky and, I imagine, discouraged way, through disabling hygiene.

set_option hygiene false in
section
  local infixr:90  " ~> " => arrow

  class Category where
    object : Type
    arrow : object → object → Type
    iden (x : object) : (x ~> x)
end

infixr:90 " ~> " => Category.arrow

[Kim Morrison]

The usual solution is to define the class in stages. For example in Mathlib we:

• define Quiver
• set up the arrow notation from that
• define Category extends Quiver, and can use the notation in the data/axioms

[Kim Morrison]

(In fact we have even more layers, with CategoryStruct for just the id/comp data, and finally Category with the axioms.)

[Eric Wieser]

Arguably the fact this helps with notation is an afterthought; in my mind the main motivation for this design is that sometimes you need to prove some very simple lemmas about the operation before you can proceed with the rest of the typeclass

[Kim Morrison]

I don't think there are any such for Quiver or CategoryStruct?

[Patrick Massot]

Also note this is a regression compared to Lean 3.

[Eric Wieser]

How so? Isn't the counter to that "you can ask for the lean3 behavior withset_option hygiene false in"?

[Patrick Massot]

In Lean you could put notations inside structure definitions.