Cosmetic issues in Lean4

Stream: lean4

[Tammo Brinner]

So i have written up a document about categories by myself in Lean4. Now i want to make it a bit cleaner by defining a symbol for composition in categories. So first of all, here is my code:

import Mathlib.Tactic
import Mathlib.Logic.Basic
import Lean.Parser
namespace mymon
set_option autoImplicit false
universe u v w u₁ v₁ u₂ v₂ u₃ v₃


/-- I should point out, that this is not the most general one can be. We could for example use Sort v and Sort u. That would allow our morphisms and objects to be Propositions etc as well. --/

structure CategoryStruct where
  Obj : Type u
  Hom : Obj → Obj → Type v
  id  : ∀ X, Hom X X
  comp : ∀ {X Y Z}, Hom Y Z → Hom X Y → Hom X Z
 -- or the appropriate module

infixl:80 " ∘ " => @CategoryStruct.comp _ _ _ _

#check  @CategoryStruct.comp _ _ _ _

variable {C : CategoryStruct} {X Y Z W : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) (h : C.Hom Z W)

#check  @C.comp X Y Z

#check h ∘ g ∘ f

#check h ∘ (g ∘ f)

#check (h ∘ g) ∘ f

structure Category extends CategoryStruct where
  comp_assoc : ∀ {W X Y Z} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z),
    toCategoryStruct.comp (toCategoryStruct.comp h g) f = toCategoryStruct.comp h (toCategoryStruct.comp g f)
  comp_id  : ∀ {X Y} (f : Hom X Y), f ∘ id X = f
  id_comp : ∀ {X Y} (f : Hom X Y), id Y ∘ f = f

I have two problems with this. The first is that #check h ∘ g ∘ f does not work as lean does not know in which order it has to evaluate this. And further, id does not seem like

$$\text{C.comp g f} = g\circ f$$

does not hold definitionally but only propositionally. This is a problem, as i would like to use the former notation in proofs for rewrites etc and the latter for cosmetic purposes. But they should really be the same! Thanks for any help in advance!

[Aaron Liu]

The elaborator is getting confused with the notation for function composition.

[Tammo Brinner]

Aaron Liu schrieb:

The elaborator is getting confused with the notation for function composition.

I fixed it