Some edits inspired by Sergey

paper/paper.md

@@ -159,8 +159,8 @@ Relatedly, `agda-stdlib` has been used as a test bed for the design of the Agda
 
 Agda’s unique support for dependently-parameterised modules [@ivardeBruin2023] has also significantly influenced the library’s design.
 Although type classes are a common mechanism for creating interfaces and overloading syntax in other functional languages such as Haskell [@haskell2010], and other ITPs like Coq and Lean's MathLib use them extensively as a core feature of their design, the developers of `agda-stdlib` has so far found little need to exploit such an approach.
-While Agda supports a very general form of instance search, the ability to use qualified, parameterised modules as first-class objects appears to reduce the need for it compared to the languages mentioned above.
-Additionally, module parameters enable the safe and scalable embedding of non-constructive mathematics into a constructive system.
+While Agda supports a very general form of instance search, the ability to use qualified, parameterised modules appears to reduce the need for it compared to the languages mentioned above.
+Additionally, parameterised modules enable the safe and scalable embedding of non-constructive mathematics into a constructive system.
 Since Agda is entirely constructive, the vast majority of `agda-stdlib` is also constructive.
 Non-constructive methods, such as classical reasoning, can be achieved by passing the relevant axioms as module parameters.
 This enables users to write provably "safe" non-constructive code, i.e. without having to *postulate* such axioms.