How does it compare to dependent records in Agda/Lean/etc.?
I heard that locales in Isabelle are used to model algebraic structures in a talk, bu. Isn't this a kind of dependent type in some sense? Is Isabelle really simply typed?
Basically, a locale is a name for a set of fixed parameters, that come with assumptions. Inside the locale, these assumptions are added implicitly to everything you define/prove. When you have concrete parameters that satisfy the assumptions, you can interpret the locale, exposing the stuff inside (instantiated for your concrete parameters).
In Isabelle, locales are quite powerful. You can base your locales on other locales, partially instantiate them, rewrite stuff, etc. (for details https://isabelle.in.tum.de/dist/Isabelle2021-1/doc/locales.pdf)