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

I recall that Conor McBride once mentioned (in the context of universe polymorphism) that "we might want to say that objects tend to be at least as large as arrows without enforcing whether or not that inequality is strict"
(https://pigworker.wordpress.com/2015/01/09/universe-hierarchies/). I guess I could have put some kind of constraint to this effect in here, but I've always just worked with the definition being polymorphic in both the level of the arrows and morphisms without any further constraint.

If I recall correctly, last time (before HoTT Agda era) that I tried to use a definition like this in my own CT scribbles, I got into problems with defining the category of functors (needed equality of natural transformations, hence function extensionality axiom).
Then, I could get away by making the equality proofs irrelevant (i.e., adding a dot before the field name of the three properties).

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.