## Stream: general

### Topic: Notation precedence

#### Kind Bubble (Jan 09 2023 at 16:26):

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 (Jan 09 2023 at 16:31):

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

#### Kind Bubble (Jan 09 2023 at 16:32):

What's the general situation?

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

#### Kind Bubble (Jan 09 2023 at 16:33):

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

#### Yaël Dillies (Jan 09 2023 at 16:34):

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

#### Kind Bubble (Jan 09 2023 at 16:36):

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

#### Kind Bubble (Jan 09 2023 at 16:45):

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 (Jan 09 2023 at 16:51):

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?

Last updated: Aug 03 2023 at 10:10 UTC