From 6e6c4a9bc2861347081ce35dc2b4716cf227518a Mon Sep 17 00:00:00 2001 From: wadler Date: Tue, 27 Mar 2018 16:14:04 -0300 Subject: [PATCH] added universe polymorphism to Equality --- src/Equality.lagda | 3 ++- src/Isomorphism.lagda | 1 + src/Lists.lagda | 2 +- 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Equality.lagda b/src/Equality.lagda index 9fc710c8..733457b2 100644 --- a/src/Equality.lagda +++ b/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) diff --git a/src/Isomorphism.lagda b/src/Isomorphism.lagda index 323e9e25..fefa2843 100644 --- a/src/Isomorphism.lagda +++ b/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 diff --git a/src/Lists.lagda b/src/Lists.lagda index f46aa5e5..bf92b57a 100644 --- a/src/Lists.lagda +++ b/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