Notation precedence

Stream: general

[Kind Bubble]

Here I have some basics of category theory. I'm in the process of establishing that the category of categories is indeed a category. I wanted F⟦f⟧ to be notation for functor application, but I can't get the notation to bind the closest. See the definition of Mor below for where I define this notation.

Goal: I want to use notations F⟦f⟧ and F⟦X⟧ for "apply functor at morphism" and "apply functor at object". I want Lean to try to match F⟦f⟧ first, then to try F⟦X⟧ (object application, see definition of FunObj), only then other functions. Is this possible?

Right now it doesn't seem to bind that way.

notation "Σ" "(" X ":" A ")" ":" F => Σ' (X : A), F
notation "Π" "(" X ":" A ")" ":" F => forall (X : A), F
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
notation "*" => Unit.unit
notation "⊛" => Unit
notation x "≡" y => Σ(_:x=y):⊛

def Refl {X : Type _} (x : X) : x≡x := PSigma.mk (Eq.refl x) *
def Symm {X : Type _} {x : X} {y : X} (f:Σ(_ : x = y):⊛):(y≡x) := PSigma.mk (Eq.symm f.1) *
def Trns {X : Type _} {x : X} {y : X} {z : X} (f : Σ(_ : x = y):⊛) (g : Σ(_ : y = z):⊛) : (x≡z):= PSigma.mk (Eq.trans f.1 g.1) *
def Push {X:Type _}{Y:Type _}{x:X}{y:X}(f:Π(_:X):Y)(p:x≡y) : (f x ≡ f y) := ⟨congrArg f p.1, *⟩

def Cat :=
Σ(Obj:Type _):
Σ(Hom:Π(_:Obj):Π(_:Obj):(Type _)):
Σ(Id:Π(X:Obj):(Hom X X)):
Σ(Cmp:Π(X:Obj):Π(Y:Obj):Π(Z:Obj):Π(_:Hom X Y):Π(_:Hom Y Z):(Hom X Z)):
Σ(_:Π(X:Obj):Π(Y:Obj):Π(f:Hom X Y):(Cmp X Y Y) f (Id Y) ≡ f):
Σ(_:Π(X:Obj):Π(Y:Obj):Π(f:Hom X Y):(Cmp X X Y) (Id X) f ≡ f):
Σ(_:Π(W:Obj):Π(X:Obj):Π(Y:Obj):Π(Z:Obj):Π(f:Hom W X):Π(g:Hom X Y):Π(h:Hom Y Z):(Cmp W X Z) f (Cmp X Y Z g h) ≡ Cmp W Y Z (Cmp W X Y f g) h):
⊛

def Obj (C : Cat) := C.1

def Hom {C : Cat }(X : Obj C)(Y : Obj C) := C.2.1 X Y

def Idn { C : Cat } (X : Obj C) := C.2.2.1 X
notation "𝟙" X => Idn X

def Cmp {C : Cat} {X : Obj C} {Y : Obj C} {Z : Obj C} (f : Hom X Y) (g : Hom Y Z) := C.2.2.2.1 X Y Z f g
notation g "∘" f => Cmp f g

def CmpIdn {C : Cat} {X : Obj C} {Y : Obj C} (f : Hom X Y) := C.2.2.2.2.2.1 X Y f

def IdnCmp {C : Cat} {X : Obj C} {Y : Obj C} (f : Hom X Y) := C.2.2.2.2.1 X Y f

def CmpCmp {C : Cat} {W : Obj C} {X : Obj C} {Y : Obj C} {Z : Obj C} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z) := C.2.2.2.2.2.2.1 W X Y Z f g h
def CatObj := Cat


def CatHom (C : Cat) (D : Cat) :=
Σ(FunObj : Π(_ : Obj C):Obj D):
Σ(FunHom : Π(X : Obj C):Π(Y : Obj C):Π(_ : Hom X Y):Hom (FunObj X) (FunObj Y)):
Σ(_ : Π(X : Obj C): FunHom X X (Idn X) ≡ Idn (FunObj X)):
Σ(_ : Π(X : Obj C):Π(Y : Obj C):Π(Z : Obj C):Π(f : Hom X Y):Π(g : Hom Y Z):Cmp (FunHom X Y f) (FunHom Y Z g) ≡ FunHom X Z (Cmp f g)):
⊛

def FunObj {C : Cat} {D : Cat} (F : CatHom C D) (X : Obj C) := F.1 X
notation F "[" X "]" => (FunObj F X)

def Mor {C : Cat} {D : Cat} {X : Obj C} {Y : Obj C} (F : CatHom C D) (f : Hom X Y) := F.2.1 X Y f
notation F "⟦" f "⟧" => Mor F f

[Yaël Dillies]

This is in fact a problem that we have tried solving for a while now.

[Kind Bubble]

What's the general situation?

Also any tips are much appreciated, as well as advice for notation here.

[Kind Bubble]

I thought I saw something where notation precedence was automatically set to 1000.

[Yaël Dillies]

We want to have coercions to functions for both docs#category_theory.functor.obj and docs#category_theory.functor.map

[Kind Bubble]

These have some good notation at least. I do like the braces though since that's more common with pen and paper.

[Kind Bubble]

nvm looks like it's just this:
https://leanprover.github.io/lean4/doc/notation.html

but I was wondering if I could overload notation here without any trouble. What if I just wanted the precedence for the morphism application to be lower (which presumably means it tries it first?).

[Kind Bubble]

Ok I tried that idea and evidently lean 4 doesn't give me any grief:

notation "Σ" "(" X ":" A ")" ":" F => Σ' (X : A), F
notation "Π" "(" X ":" A ")" ":" F => forall (X : A), F
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
notation "*" => Unit.unit
notation "⊛" => Unit
notation x "≡" y => Σ(_:x=y):⊛
def Refl {X : Type _} (x : X) : x≡x := PSigma.mk (Eq.refl x) *
def Symm {X : Type _} {x : X} {y : X} (f:Σ(_ : x = y):⊛):(y≡x) := PSigma.mk (Eq.symm f.1) *
notation "-" p => Symm p
def Trns {X : Type _} {x : X} {y : X} {z : X} (f : Σ(_ : x = y):⊛) (g : Σ(_ : y = z):⊛) : (x≡z):= PSigma.mk (Eq.trans f.1 g.1) *
notation p "~" q => Trns p q
def Push {X:Type _}{Y:Type _}{x:X}{y:X}(f:Π(_:X):Y)(p:x≡y) : (f x ≡ f y) := ⟨congrArg f p.1, *⟩
def Cat :=
Σ(Obj:Type _):
Σ(Hom:Π(_:Obj):Π(_:Obj):(Type _)):
Σ(Id:Π(X:Obj):(Hom X X)):
Σ(Cmp:Π(X:Obj):Π(Y:Obj):Π(Z:Obj):Π(_:Hom X Y):Π(_:Hom Y Z):(Hom X Z)):
Σ(_:Π(X:Obj):Π(Y:Obj):Π(f:Hom X Y):(Cmp X Y Y) f (Id Y) ≡ f):
Σ(_:Π(X:Obj):Π(Y:Obj):Π(f:Hom X Y):(Cmp X X Y) (Id X) f ≡ f):
Σ(_:Π(W:Obj):Π(X:Obj):Π(Y:Obj):Π(Z:Obj):Π(f:Hom W X):Π(g:Hom X Y):Π(h:Hom Y Z):(Cmp W X Z) f (Cmp X Y Z g h) ≡ Cmp W Y Z (Cmp W X Y f g) h):
⊛

def Obj (C : Cat) := C.1

def Hom {C : Cat }(X : Obj C)(Y : Obj C) := C.2.1 X Y

def Idn { C : Cat } (X : Obj C) := C.2.2.1 X
notation "𝟙" X => Idn X /-REVISE-/

def Cmp {C : Cat} {X : Obj C} {Y : Obj C} {Z : Obj C} (f : Hom X Y) (g : Hom Y Z) := C.2.2.2.1 X Y Z f g
notation g "∘" f => Cmp f g

def CmpIdn {C : Cat} {X : Obj C} {Y : Obj C} (f : Hom X Y) := C.2.2.2.2.2.1 X Y f

def IdnCmp {C : Cat} {X : Obj C} {Y : Obj C} (f : Hom X Y) := C.2.2.2.2.1 X Y f

def CmpCmp {C : Cat} {W : Obj C} {X : Obj C} {Y : Obj C} {Z : Obj C} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z) := C.2.2.2.2.2.2.1 W X Y Z f g h
def CatObj := Cat


def CatHom (C : Cat) (D : Cat) :=
Σ(FunObj : Π(_ : Obj C):Obj D):
Σ(FunHom : Π(X : Obj C):Π(Y : Obj C):Π(_ : Hom X Y):Hom (FunObj X) (FunObj Y)):
Σ(_ : Π(X : Obj C): FunHom X X (Idn X) ≡ Idn (FunObj X)):
Σ(_ : Π(X : Obj C):Π(Y : Obj C):Π(Z : Obj C):Π(f : Hom X Y):Π(g : Hom Y Z):Cmp (FunHom X Y f) (FunHom Y Z g) ≡ FunHom X Z (Cmp f g)):
⊛

def FunObj {C : Cat} {D : Cat} (F : CatHom C D) (X : Obj C) := F.1 X
notation:3 F "[" X:4 "]" => FunObj F X

def Mor {C : Cat} {D : Cat} {X : Obj C} {Y : Obj C} (F : CatHom C D) (f : Hom X Y) := F.2.1 X Y f
notation:1 F "[" f:2 "]" => Mor F f

def FunIdn {C : Cat} {D : Cat} (F : CatHom C D) (X : Obj C) := F.2.2.1 X

def FunCmp {C : Cat} {D : Cat} {X : Obj C} {Y : Obj C} {Z : Obj C} (F : CatHom C D) (f : Hom X Y) (g : Hom Y Z) := F.2.2.2.1 X Y Z f g

def CatIdn (C : Cat) : CatHom C C :=
⟨
(X : Obj C)↦X,
(X : Obj C)↦(Y : Obj C)↦(f : Hom X Y)↦f,
(X : Obj C)↦Refl (Idn X),
(X : Obj C)↦(Y : Obj C)↦(Z : Obj C)↦(f : Hom X Y)↦(g : Hom Y Z)↦Refl (Cmp f g),
*
⟩
def CatCmp (C : Cat) (D : Cat) (E : Cat) (F : CatHom C D) (G : CatHom D E) : (CatHom C E) :=
⟨
(X : Obj C)↦(G.1) ((F.1) X),
(X : Obj C)↦(Y : Obj C)↦(f : Hom X Y)↦(G.2.1) (F.1 X) (F.1 Y) ((F.2.1) X Y f),
(X : Obj C)↦Trns ( Push (G.2.1 (F.1 X) (F.1 X)) (F.2.2.1 X) ) ((G.2.2.1) (F.1 X)),
(X : Obj C)↦(Y : Obj C)↦(Z : Obj C)↦(f : Hom X Y)↦(g : Hom Y Z)↦
(
Trns
(FunCmp G  (F[f]) (F[g]))
(Push (G.2.1 (F[X]) (F[Z])) (FunCmp F f g))
),
*⟩

Notice how I used the F[X] and F[f] notations in the lines near the bottom.

I'm not sure if this is unrecommended or not. Evidently it works?