Refactoring category

Stream: maths

[Attila Vajda]

Please help with tips for refactoring this category, because I am learning to construct object-and arrows foundations in Lean4. For example, I would like to prove a≅a, or every identity arrow is iso, and things like that, so I thought maybe it is fun to write these in Lean4.

Is the deriving useful to have?

structure Object where
  name : String
deriving DecidableEq, Repr

structure Arrow where
  f   : String
  dom : Object
  cod : Object
deriving Repr

namespace Cat

def id (o : Object) : Arrow := { f := "id_" ++ o.name, dom := o, cod := o }

def comp (f g : Arrow) : Option Arrow :=
  if f.cod = g.dom then some { f := f.f ++ g.f, dom := f.dom, cod := g.cod } else none

axiom assoc (f g h : Arrow) : (comp f g >>= fun fg => comp fg h) = (comp g h >>= fun gh => comp f gh)
axiom unit_l (f : Arrow) : comp (id f.dom) f = some f
axiom unit_r (f : Arrow) : comp f (id f.cod) = some f

end Cat

def a : Object := { name := "a" }
def b : Object := { name := "b" }
def c : Object := { name := "c" }

def f : Arrow := { f := "f", dom := a, cod := b }
def g : Arrow := { f := "g", dom := b, cod := c }

#eval match C.comp f g with
      | some h => h.f
      | none   => "undef"  -- prints "fg"

referece: Saunders Mac Lane - Categories
Bildschirmfoto 2025-11-16 um 08.55.17.png
Bildschirmfoto 2025-11-16 um 08.55.31.png

[Chris Henson]

Have you looked at Mathlib's docs#CategoryTheory.Category already? There you will see for instance how to avoid needing to check for compatible (co)domains in defining composition.

[Attila Vajda]

Chris Henson said:

Have you looked at Mathlib's docs#CategoryTheory.Category already? There you will see for instance how to avoid needing to check for compatible (co)domains in defining composition.

Not yet! Thanks for the tip I will check docs