This is probably a very stupid question, but i can not seem to figure out how categories are really implemented in Lean4. So from what i have seen so far, you need two universes u and v. One, which specifies the universe the objects live in and one, which specifies in which universe the morphisms live in. In order to give an instance of a category, i thought you would need to say what the objects and the morphisms (also identity) are and what the composition does. Usually you would need to prove that it is associative etc but the implementation does this for you somehow. Could someone maybe help me and give me an instance of the Category of groups or algebras and explain why it works?
This is what i thought would work. I think v can be inferred by lean, just because i have given the type of elements in Hom. But i get a cryptic error here.
instance CategoryOfSets : LargeCategory (Type u) :=
{
-- Morphisms are functions between types
Hom := fun (X Y : Type u) ↦ X → Y,
-- Identity morphism for each type is the identity function
id := fun (X : Type u) ↦ id,
-- Composition of functions
comp := fun (X Y Z : Type u) (f : X → Y) (g : Y → Z) ↦ f ≫ g,
}
The problem is that you're using the notation ≫ for composition, which already assumes a category instance. The solution is to use g ∘ f instead, which is composition of functions. Otherwise your understanding of the implementation of categories in mathlib seems correct to me (regarding associativity etc, it tries to prove them automatically, but if it fails, you have to do it yourself).
The following works (note also the nice where syntax):
import Mathlib
open CategoryTheory
instance CategoryOfSets : LargeCategory (Type u) where
Hom X Y := X → Y
id X := id
comp f g := g ∘ f