Definition of a category as an Agda record: level polymorphic in the objects and arrows

Category.agda

module Category where

open import Level
open import Relation.Binary.PropositionalEquality

open Level

record Category {lobj : Level} {larr : Level} : Set (suc (lobj ⊔ larr)) where
  field obj : Set lobj
        arr : (src : obj) -> (trg : obj) -> Set larr

        -- composition in the left-to-right form
        _$_ : {a b c : obj} (f : arr a b) -> (g : arr b c) -> arr a c
        id  : (a : obj) -> arr a a

        -- Properties of associativity/identity
        comp-assoc : {a b c d : obj} (f : arr a b) (g : arr b c) (h : arr c d) -> (f $ (g $ h)) ≡ ((f $ g) $ h)
        id-right : {a b : obj} {f : arr a b} -> (f $ (id b)) ≡ f
        id-left : {a b : obj} {f : arr a b} -> ((id a) $ f) ≡ f        

-- Lift Agda "Set" into a category.

setCat : Category {suc zero} {zero}
setCat = record
            { obj = Set
            ; arr = λ src trg → src -> trg
            ; _$_ = λ f g x → g (f x)
            ; id = λ a x → x
            ; comp-assoc = λ f g h → refl
            ; id-right = refl
            ; id-left = refl
            }

open Category

Take a close look at the definition of Category in copumpkin's excellent library (https://github.com/copumpkin/categories). As @shayan-najd comments, your definition will not scale to higher categorical stuff.

Yes this looks nice- making it parametric on the equality theory is certainly useful.