order of operations for ∘

Stream: general

[Dean Young]

(deleted)

[Dean Young]

universe u
universe v


-- Definition of a category
structure categories where
  Obj : Type u
  Hom : ∀(_:Obj),∀(_:Obj), Type v
  identity : ∀(X:Obj),Hom X X
  composition : ∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(_:Hom X Y),∀(_:Hom Y Z),Hom X Z
  identity₁: ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(composition X Y Y) f (identity Y) = f
  identity₂: ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(composition X X Y) (identity X) f = f
  associativity : ∀(W:Obj),∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(f:Hom W X),∀(g:Hom X Y),∀(h:Hom Y Z),
  (composition W X Z) f (composition X Y Z g h) = composition W Y Z (composition W X Y f g) h

-- Obj notation which infers the category in which the hom Type resides
def Obj (C : categories) := C.Obj

-- Hom notation which infers the category in which the hom Type resides
def Hom {C : categories} (X : C.Obj) (Y : C.Obj) := C.Hom X Y

-- Identity morphism notation which infers the category in which the identity morphism resides
def Idn {C : categories} (X : C.Obj) := C.identity X

-- Composition notation which infers the category, domains, and codomains involved
def composition {C : categories} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) := C.composition X Y Z f g
notation g "∘" f => composition f g

I'm using the ∘ notation for my categories (see last line above).

Unfortunately, I routinely need to add parenthesis especially when dealing with = (equality type). Can someone help me modify my composition notation so that I don't need parentheses when dealing with =?

Here's the relevant line:

notation g "∘" f => composition f g

[Kevin Buzzard]

docs#function.comp

[Kevin Buzzard]

infixr ` ∘ `:90  := function.comp

Try that -- it's what core Lean does (I just checked by following the above link and viewing source). The 90 is a bigger binding power than what you're using (I assume; I don't know what default binding power is).