I'm fairly new to Lean, so apologies if this is obvious. I'm trying to learn Lean and category theory, by doing some category theory exercises in Lean. I have these definitions for arrows and categories:
variable {α : Type u}
inductive Arrow : α → α → Type u
| Id (x : α) : Arrow x x
| Comp (g : Arrow b c) (f : Arrow a b) : Arrow a c
notation a " -→ " b => Arrow a b
notation a " ∘ " b => Arrow.Comp a b
structure Category :=
(assoc {a b c d : α} : ∀ (f : a -→ b) (g : b -→ c) (k : c -→ d),
(k ∘ (g ∘ f)) = ((k ∘ g) ∘ f))
(unitl {a b : α} : ∀ (f : a -→ b), ((Arrow.Id b) ∘ f) = f)
(unitr {a b : α} : ∀ (f : a -→ b), (f ∘ (Arrow.Id a)) = f)
This all compiles fine, so I try to define a discrete category as follows:
def IsDiscrete :=
∀ (x y : α) (f : Arrow x y), x = y ∧ f = Arrow.Id x
The intent is to express "all arrows are identity arrows", but the compiler complains that f has type "Arrow x y", not "Arrow x x". Of course, the whole point is that if arrow f exists, then x = y, so the comparison between f and Id x is sensible. How do I express this in Lean?
Alternatively, is there a better way to express arrows and/or categories in Lean? If so, why is that way better?