added universe polymorphism to Equality

src/Equality.lagda

@@ -400,7 +400,7 @@ Nonetheless, rewrite is a vital part of the Agda toolkit,
 as earlier examples have shown.
 
 
-## Extensionality {!#extensionality}
+## Extensionality {#extensionality}
 
 Extensionality asserts that they only way to distinguish functions is
 by applying them; if two functions applied to the same argument always
@@ -624,3 +624,4 @@ This chapter uses the following unicode.
     ⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
     ∎  U+220E  END OF PROOF (\qed)
     ≐  U+2250  APPROACHES THE LIMIT (\.=)
+    ℓ  U+2113  SCRIPT SMALL L (\ell)

src/Isomorphism.lagda

@@ -17,6 +17,7 @@ distributivity.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong; cong-app)
 open Eq.≡-Reasoning
+open Level
 \end{code}
 
 ## Function composition

src/Lists.lagda

@@ -851,7 +851,7 @@ replacement for `_×_`.  As a consequence, demonstrate an isomorphism relating
 
 ### Exercise (`¬Any≃All¬`)
 
-We first generalise composition to arbitrary levels, using
+First generalise composition to arbitrary levels, using
 [universe polymorphism][unipoly].
 \begin{code}
 _∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃} → (B → C) → (A → B) → A → C