diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda index 3c65e60dff..86a59aca14 100644 --- a/src/Data/List/Relation/Unary/All.agda +++ b/src/Data/List/Relation/Unary/All.agda @@ -115,7 +115,7 @@ zip = zipWith id unzip : All (P ∩ Q) ⊆ All P ∩ All Q unzip = unzipWith id -module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where +module _ (S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where open Setoid S renaming (refl to ≈-refl) open SetoidMembership S