[ fix #1313 ] List/**/All/Properties.map-id has too many parameters (#1314)

Author: ajrouvoet

CHANGELOG.md

@@ -9,6 +9,9 @@ Highlights
 Bug-fixes
 ---------
 
+* Fixed List.Relation.Unary.All.Properties.map-id, which was abstracted over
+  unused module parameters.
+
 Non-backwards compatible changes
 --------------------------------
 

src/Data/List/Relation/Unary/All/Properties.agda

@@ -173,17 +173,19 @@ module _ {P : A → Set p} where
 ------------------------------------------------------------------------
 -- map
 
+module _ {P : Pred A p} where
+
+  map-id : ∀ {xs} (pxs : All P xs) → All.map id pxs ≡ pxs
+  map-id []         = refl
+  map-id (px ∷ pxs) = cong (px ∷_)  (map-id pxs)
+
 module _ {P : Pred A p} {Q : Pred A q} {f : P ⋐ Q} where
 
   map-cong : ∀ {xs} {g : P ⋐ Q} (pxs : All P xs) →
              (∀ {x} → f {x} ≗ g) → All.map f pxs ≡ All.map g pxs
   map-cong []         _   = refl
   map-cong (px ∷ pxs) feq = cong₂ _∷_ (feq px) (map-cong pxs feq)
 
-  map-id : ∀ {xs} (pxs : All P xs) → All.map id pxs ≡ pxs
-  map-id []         = refl
-  map-id (px ∷ pxs) = cong (px ∷_)  (map-id pxs)
-
   map-compose : ∀ {r} {R : Pred A r} {xs} {g : Q ⋐ R} (pxs : All P xs) →
                 All.map g (All.map f pxs) ≡ All.map (g ∘ f) pxs
   map-compose []         = refl