Advice on coding a simple category?

Stream: lean4

[Mark Wilhelm]

I'm trying to encode a simple little category like so --

inductive Obj :=
  | Manager
  | Employee
  | Department
open Obj

inductive Hom: Obj -> Obj -> Type :=
  | idt (o: Obj) : Hom o o
  | com {a b c: Obj} (f: Hom a b) (g: Hom b c) : Hom a c
  | managedBy: Hom Employee Manager
  | managesIn: Hom Manager Department
  | worksIn: Hom Employee Department
open Hom
infixl:65 " ; " => com

...now if I want to say something like managedBy ; managesIn = worksIn, seems like I could:

1. use axioms
2. have a new function that takes two elements of Hom a b and gives back a Prop
3. provide an instance of the Eq typeclass for Hom a b
4. some other option

(and I think I would also use this method for having associativity and identity properties be true "by definition"). I was not able to find syntax that works for option 3, although it seemed like that would be the right choice. Any advice? thanks

[Horațiu Cheval]

Option 1 would be unsound as it is provably the case that com ... ≠ worksIn ... if they are both constructors

[Reid Barton]

There's no Eq type class. = is the actual propositional equality, and the equations that you want don't hold of course.
Options are to put an equivalence relation on each Hom a b, and form the docs4#Quotient; or, in this case, just don't introduce the redundant representations of what you want to be the "same" morphism in the first place.

[Mark Wilhelm]

Ok then it looks like to do the quotient approach, I define an instance of the Setoid typeclass for Hom a b, which I then use to define a Quotient, and then I would use that quotient instead of using Hom a b directly?

[Trebor Huang]

You can also try 4: Instead of making idt and com constructors, you define Arrow to be the rest of the constructors, and define ListOfArrowsThatAreComposable inductively, almost like a list. So then the empty list is idt, and concatenation of lists serve as the composition. Note that in this way no quotienting is required, and everything is computable. I'm sure this is already done in mathlib, search for "free category generated by quivers"

[Trebor Huang]

docs#quiver.path