[ refactor ] Data.List.Relation.Unary.Enumerates.Setoid.Properties using tighter lemma from Function.Consequences

src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda

@@ -6,6 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
+module Data.List.Relation.Unary.Enumerates.Setoid.Properties where
+
 open import Data.List.Base
 open import Data.List.Membership.Setoid.Properties as Membership
 open import Data.List.Relation.Unary.Any using (index)
@@ -14,32 +16,32 @@ open import Data.List.Relation.Unary.Enumerates.Setoid
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Sum.Relation.Binary.Pointwise
   using (_⊎ₛ_; inj₁; inj₂)
-open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
   using (_×ₛ_)
 open import Function.Base using (_∘_)
 open import Function.Bundles using (Surjection)
 open import Function.Definitions using (Surjective)
-open import Function.Consequences using (strictlySurjective⇒surjective)
+open import Function.Consequences using (inverseˡ⇒surjective)
 open import Level
 open import Relation.Binary.Bundles using (Setoid; DecSetoid)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.Properties.Setoid using (respʳ-flip)
 
-module Data.List.Relation.Unary.Enumerates.Setoid.Properties where
-
-
 private
   variable
     a b ℓ₁ ℓ₂ : Level
+    A : Set a
+    xs ys : List A
+
 
 ------------------------------------------------------------------------
 -- map
 
 module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) (surj : Surjection S T) where
   open Surjection surj
 
-  map⁺ : ∀ {xs} → IsEnumeration S xs → IsEnumeration T (map to xs)
+  map⁺ : IsEnumeration S xs → IsEnumeration T (map to xs)
   map⁺ _∈xs y with (x , fx≈y) ← strictlySurjective y =
       ∈-resp-≈ T fx≈y (∈-map⁺ S T cong (x ∈xs))
 
@@ -48,15 +50,15 @@ module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) (surj : Surjection S T) whe
 
 module _ (S : Setoid a ℓ₁) where
 
-  ++⁺ˡ : ∀ {xs} ys → IsEnumeration S xs → IsEnumeration S (xs ++ ys)
+  ++⁺ˡ : ∀ ys → IsEnumeration S xs → IsEnumeration S (xs ++ ys)
   ++⁺ˡ _ _∈xs v = Membership.∈-++⁺ˡ S (v ∈xs)
 
-  ++⁺ʳ : ∀ xs {ys} → IsEnumeration S ys → IsEnumeration S (xs ++ ys)
+  ++⁺ʳ : ∀ xs → IsEnumeration S ys → IsEnumeration S (xs ++ ys)
   ++⁺ʳ _ _∈ys v = Membership.∈-++⁺ʳ S _ (v ∈ys)
 
 module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) where
 
-  ++⁺ : ∀ {xs ys} → IsEnumeration S xs → IsEnumeration T ys →
+  ++⁺ : IsEnumeration S xs → IsEnumeration T ys →
         IsEnumeration (S ⊎ₛ T) (map inj₁ xs ++ map inj₂ ys)
   ++⁺ _∈xs _ (inj₁ x) = ∈-++⁺ˡ (S ⊎ₛ T)   (∈-map⁺ S (S ⊎ₛ T) inj₁ (x ∈xs))
   ++⁺ _ _∈ys (inj₂ y) = ∈-++⁺ʳ (S ⊎ₛ T) _ (∈-map⁺ T (S ⊎ₛ T) inj₂ (y ∈ys))
@@ -66,7 +68,7 @@ module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) where
 
 module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) where
 
-  cartesianProduct⁺ : ∀ {xs ys} → IsEnumeration S xs → IsEnumeration T ys →
+  cartesianProduct⁺ : IsEnumeration S xs → IsEnumeration T ys →
                       IsEnumeration (S ×ₛ T) (cartesianProduct xs ys)
   cartesianProduct⁺ _∈xs _∈ys (x , y) = ∈-cartesianProduct⁺ S T (x ∈xs) (y ∈ys)
 
@@ -76,17 +78,15 @@ module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) where
 module _ (S? : DecSetoid a ℓ₁) where
   open DecSetoid S? renaming (setoid to S)
 
-  deduplicate⁺ : ∀ {xs} → IsEnumeration S xs →
-                 IsEnumeration S (deduplicate _≟_ xs)
+  deduplicate⁺ : IsEnumeration S xs → IsEnumeration S (deduplicate _≟_ xs)
   deduplicate⁺ = ∈-deduplicate⁺ S _≟_ (respʳ-flip S) ∘_
 
 ------------------------------------------------------------------------
 -- lookup
 
 module _ (S : Setoid a ℓ₁) where
-  open Setoid S
+  open Setoid S using (_≈_; sym)
 
-  lookup-surjective : ∀ {xs} → IsEnumeration S xs →
-                      Surjective _≡_ _≈_ (lookup xs)
-  lookup-surjective _∈xs = strictlySurjective⇒surjective
-    trans (λ { ≡.refl → refl}) (λ y → index (y ∈xs) , sym (lookup-index (y ∈xs)))
+  lookup-surjective : IsEnumeration S xs → Surjective _≡_ _≈_ (lookup xs)
+  lookup-surjective _∈xs = inverseˡ⇒surjective _≈_
+    λ where ≡.refl → sym (lookup-index (_ ∈xs))