Remove implicit parameters from Sublist.Propositional.Properties (agda#2514)

* Remove implicit parameters from Sublist.Propositional.Properties

* Addressed James' feedback

* Fixed whitespace

Author: MatthewDaggitt

CHANGELOG.md

@@ -19,7 +19,9 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
-In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold.
+* In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold.
+
+* In `Data.List.Relation.Binary.Sublist.Propositional.Properties` the implicit module parameters `a` and `A` have been replaced with `variable`s. This should be a backwards compatible change for the overwhelming majority of uses, and would only be non-backwards compatible if you were explicitly supplying these implicit parameters for some reason when importing the module. Explicitly supplying the implicit parameters for functions exported from the module should not be affected.
 
 Minor improvements
 ------------------

src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda

@@ -6,8 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Data.List.Relation.Binary.Sublist.Propositional.Properties
-  {a} {A : Set a} where
+module Data.List.Relation.Binary.Sublist.Propositional.Properties where
 
 open import Data.List.Base using (List; []; _∷_;  map)
 open import Data.List.Membership.Propositional using (_∈_)
@@ -31,54 +30,54 @@ open import Relation.Unary using (Pred)
 
 private
   variable
-    b ℓ : Level
-    B : Set b
+    a ℓ : Level
+    A B : Set a
+    x y : A
+    ws xs ys zs : List A
 
 ------------------------------------------------------------------------
 -- Re-exporting setoid properties
 
-open SetoidProperties (setoid A) public
-  hiding (map⁺; ⊆-trans-idˡ; ⊆-trans-idʳ; ⊆-trans-assoc)
+module _ {A : Set a} where
+  open SetoidProperties  (setoid A) public
+    hiding (map⁺; ⊆-trans-idˡ; ⊆-trans-idʳ; ⊆-trans-assoc)
 
-map⁺ : ∀ {as bs} (f : A → B) → as ⊆ bs → map f as ⊆ map f bs
-map⁺ {B = B} f = SetoidProperties.map⁺ (setoid A) (setoid B) (cong f)
+map⁺ : (f : A → B) → xs ⊆ ys → map f xs ⊆ map f ys
+map⁺ f = SetoidProperties.map⁺ (setoid _) (setoid _) (cong f)
 
 ------------------------------------------------------------------------
 -- Category laws for _⊆_
 
-⊆-trans-idˡ : ∀ {xs ys : List A} {τ : xs ⊆ ys} →
-              ⊆-trans ⊆-refl τ ≡ τ
-⊆-trans-idˡ {τ = τ} = SetoidProperties.⊆-trans-idˡ (setoid A) (λ _ → refl) τ
+⊆-trans-idˡ : ∀ {τ : xs ⊆ ys} → ⊆-trans ⊆-refl τ ≡ τ
+⊆-trans-idˡ {τ = τ} = SetoidProperties.⊆-trans-idˡ (setoid _) (λ _ → refl) τ
 
-⊆-trans-idʳ : ∀ {xs ys : List A} {τ : xs ⊆ ys} →
-              ⊆-trans τ ⊆-refl ≡ τ
-⊆-trans-idʳ {τ = τ} = SetoidProperties.⊆-trans-idʳ (setoid A) trans-reflʳ τ
+⊆-trans-idʳ : ∀ {τ : xs ⊆ ys} → ⊆-trans τ ⊆-refl ≡ τ
+⊆-trans-idʳ {τ = τ} = SetoidProperties.⊆-trans-idʳ (setoid _) trans-reflʳ τ
 
 -- Note: The associativity law is oriented such that rewriting with it
 -- may trigger reductions of ⊆-trans, which matches first on its
 -- second argument and then on its first argument.
 
-⊆-trans-assoc : ∀ {ws xs ys zs : List A}
-                {τ₁ : ws ⊆ xs} {τ₂ : xs ⊆ ys} {τ₃ : ys ⊆ zs} →
+⊆-trans-assoc : ∀ {τ₁ : ws ⊆ xs} {τ₂ : xs ⊆ ys} {τ₃ : ys ⊆ zs} →
                 ⊆-trans τ₁ (⊆-trans τ₂ τ₃) ≡ ⊆-trans (⊆-trans τ₁ τ₂) τ₃
 ⊆-trans-assoc {τ₁ = τ₁} {τ₂ = τ₂} {τ₃ = τ₃} =
-  SetoidProperties.⊆-trans-assoc (setoid A) (λ p _ _ → ≡.sym (trans-assoc p)) τ₁ τ₂ τ₃
+  SetoidProperties.⊆-trans-assoc (setoid _) (λ p _ _ → ≡.sym (trans-assoc p)) τ₁ τ₂ τ₃
 
 ------------------------------------------------------------------------
 -- Laws concerning ⊆-trans and ∷ˡ⁻
 
-⊆-trans-∷ˡ⁻ᵣ : ∀ {y} {xs ys zs : List A} {τ : xs ⊆ ys} {σ : (y ∷ ys) ⊆ zs} →
+⊆-trans-∷ˡ⁻ᵣ : ∀ {τ : xs ⊆ ys} {σ : (y ∷ ys) ⊆ zs} →
                ⊆-trans τ (∷ˡ⁻ σ) ≡ ⊆-trans (y ∷ʳ τ) σ
 ⊆-trans-∷ˡ⁻ᵣ {σ = x ∷ σ} = refl
 ⊆-trans-∷ˡ⁻ᵣ {σ = y ∷ʳ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ᵣ
 
-⊆-trans-∷ˡ⁻ₗ : ∀ {x} {xs ys zs : List A} {τ : (x ∷ xs) ⊆ ys} {σ : ys ⊆ zs} →
+⊆-trans-∷ˡ⁻ₗ : ∀ {τ : (x ∷ xs) ⊆ ys} {σ : ys ⊆ zs} →
               ⊆-trans (∷ˡ⁻ τ) σ ≡ ∷ˡ⁻ (⊆-trans τ σ)
 ⊆-trans-∷ˡ⁻ₗ                {σ = y   ∷ʳ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ₗ
 ⊆-trans-∷ˡ⁻ₗ {τ = y   ∷ʳ τ} {σ = refl ∷ σ} = cong (y ∷ʳ_) ⊆-trans-∷ˡ⁻ₗ
 ⊆-trans-∷ˡ⁻ₗ {τ = refl ∷ τ} {σ = refl ∷ σ} = refl
 
-⊆-∷ˡ⁻trans-∷ : ∀ {y} {xs ys zs : List A} {τ : xs ⊆ ys} {σ : (y ∷ ys) ⊆ zs} →
+⊆-∷ˡ⁻trans-∷ : ∀ {τ : xs ⊆ ys} {σ : (y ∷ ys) ⊆ zs} →
                ∷ˡ⁻ (⊆-trans (refl ∷ τ) σ) ≡ ⊆-trans (y ∷ʳ τ) σ
 ⊆-∷ˡ⁻trans-∷ {σ = y   ∷ʳ σ} = cong (y ∷ʳ_) ⊆-∷ˡ⁻trans-∷
 ⊆-∷ˡ⁻trans-∷ {σ = refl ∷ σ} = refl
@@ -103,14 +102,14 @@ Any-resp-⊆ = lookup
 
 -- First functor law: identity.
 
-All-resp-⊆-refl : ∀ {P : Pred A ℓ} {xs : List A} →
+All-resp-⊆-refl : ∀ {P : Pred A ℓ} →
                   All-resp-⊆ ⊆-refl ≗ id {A = All P xs}
 All-resp-⊆-refl []       = refl
 All-resp-⊆-refl (p ∷ ps) = cong (p ∷_) (All-resp-⊆-refl ps)
 
 -- Second functor law: composition.
 
-All-resp-⊆-trans : ∀ {P : Pred A ℓ} {xs ys zs} {τ : xs ⊆ ys} (τ′ : ys ⊆ zs) →
+All-resp-⊆-trans : ∀ {P : Pred A ℓ} {τ : xs ⊆ ys} (τ′ : ys ⊆ zs) →
                    All-resp-⊆ {P = P} (⊆-trans τ τ′) ≗ All-resp-⊆ τ ∘ All-resp-⊆ τ′
 All-resp-⊆-trans                (_    ∷ʳ τ′) (p ∷ ps) = All-resp-⊆-trans τ′ ps
 All-resp-⊆-trans {τ = _ ∷ʳ _  } (refl ∷  τ′) (p ∷ ps) = All-resp-⊆-trans τ′ ps
@@ -122,7 +121,7 @@ All-resp-⊆-trans {τ = []      } ([]        ) []       = refl
 
 -- First functor law: identity.
 
-Any-resp-⊆-refl : ∀ {P : Pred A ℓ} {xs} →
+Any-resp-⊆-refl : ∀ {P : Pred A ℓ} →
                   Any-resp-⊆ ⊆-refl ≗ id {A = Any P xs}
 Any-resp-⊆-refl (here p)  = refl
 Any-resp-⊆-refl (there i) = cong there (Any-resp-⊆-refl i)
@@ -131,7 +130,7 @@ lookup-⊆-refl = Any-resp-⊆-refl
 
 -- Second functor law: composition.
 
-Any-resp-⊆-trans : ∀ {P : Pred A ℓ} {xs ys zs} {τ : xs ⊆ ys} (τ′ : ys ⊆ zs) →
+Any-resp-⊆-trans : ∀ {P : Pred A ℓ} {τ : xs ⊆ ys} (τ′ : ys ⊆ zs) →
                    Any-resp-⊆ {P = P} (⊆-trans τ τ′) ≗ Any-resp-⊆ τ′ ∘ Any-resp-⊆ τ
 Any-resp-⊆-trans                (_ ∷ʳ τ′) i         = cong there (Any-resp-⊆-trans τ′ i)
 Any-resp-⊆-trans {τ = _   ∷ʳ _} (_ ∷  τ′) i         = cong there (Any-resp-⊆-trans τ′ i)
@@ -147,7 +146,7 @@ lookup-⊆-trans = Any-resp-⊆-trans
 -- Note: `lookup` can be seen as a strictly increasing reindexing
 -- function for indices into `xs`, producing indices into `ys`.
 
-lookup-injective : ∀ {P : Pred A ℓ} {xs ys} {τ : xs ⊆ ys} {i j : Any P xs} →
+lookup-injective : ∀ {P : Pred A ℓ} {τ : xs ⊆ ys} {i j : Any P xs} →
                    lookup τ i ≡ lookup τ j → i ≡ j
 lookup-injective {τ = _  ∷ʳ _}                     = lookup-injective ∘′ there-injective
 lookup-injective {τ = x≡y ∷ _} {here  _} {here  _} = cong here ∘′ subst-injective x≡y ∘′ here-injective
@@ -163,12 +162,12 @@ lookup-injective {τ = _   ∷ _} {there _} {there _} = cong there ∘′ lookup
 -- Note: This lemma does not hold for Sublist.Setoid, but could hold for
 -- a hypothetical Sublist.Groupoid where trans refl = id.
 
-from∈∘to∈ : ∀ {x : A} {xs ys} (τ : x ∷ xs ⊆ ys) →
+from∈∘to∈ : ∀ (τ : x ∷ xs ⊆ ys) →
             from∈ (to∈ τ) ≡ ⊆-trans (refl ∷ minimum xs) τ
 from∈∘to∈ (x≡y ∷ τ) = cong (x≡y ∷_) ([]⊆-irrelevant _ _)
 from∈∘to∈ (y  ∷ʳ τ) = cong (y  ∷ʳ_) (from∈∘to∈ τ)
 
-from∈∘lookup : ∀{x : A} {xs ys} (τ : xs ⊆ ys) (i : x ∈ xs) →
+from∈∘lookup : ∀ (τ : xs ⊆ ys) (i : x ∈ xs) →
                from∈ (lookup τ i) ≡ ⊆-trans (from∈ i) τ
 from∈∘lookup (y   ∷ʳ τ)  i          = cong (y ∷ʳ_) (from∈∘lookup τ i)
 from∈∘lookup (_    ∷ τ) (there i)   = cong (_ ∷ʳ_) (from∈∘lookup τ i)
@@ -179,15 +178,14 @@ from∈∘lookup (refl ∷ τ) (here refl) = cong (refl ∷_) ([]⊆-irrelevant
 
 -- A raw pushout is a weak pushout if the pushout square commutes.
 
-IsWeakPushout : ∀{xs ys zs : List A} {τ : xs ⊆ ys} {σ : xs ⊆ zs} →
-                RawPushout τ σ → Set a
+IsWeakPushout : ∀ {τ : xs ⊆ ys} {σ : xs ⊆ zs} → RawPushout τ σ → Set _
 IsWeakPushout {τ = τ} {σ = σ} rpo =
   ⊆-trans τ (RawPushout.leg₁ rpo) ≡
   ⊆-trans σ (RawPushout.leg₂ rpo)
 
 -- Joining two list extensions with ⊆-pushout produces a weak pushout.
 
-⊆-pushoutˡ-is-wpo : ∀{xs ys zs : List A} (τ : xs ⊆ ys) (σ : xs ⊆ zs) →
+⊆-pushoutˡ-is-wpo : ∀ (τ : xs ⊆ ys) (σ : xs ⊆ zs) →
                     IsWeakPushout (⊆-pushoutˡ τ σ)
 ⊆-pushoutˡ-is-wpo [] σ
   rewrite ⊆-trans-idʳ {τ = σ}
@@ -201,7 +199,7 @@ IsWeakPushout {τ = τ} {σ = σ} rpo =
 
 -- From τ₁ ⊎ τ₂ = τ, compute the injection ι₁ such that τ₁ = ⊆-trans ι₁ τ.
 
-DisjointUnion-inj₁ : ∀ {xs ys zs xys : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} →
+DisjointUnion-inj₁ : ∀ {xys : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} →
                       DisjointUnion τ₁ τ₂ τ → ∃ λ (ι₁ : xs ⊆ xys) → ⊆-trans ι₁ τ ≡ τ₁
 DisjointUnion-inj₁ []         = []       , refl
 DisjointUnion-inj₁ (y   ∷ₙ d) = _        , cong (y  ∷ʳ_) (proj₂ (DisjointUnion-inj₁ d))
@@ -210,7 +208,7 @@ DisjointUnion-inj₁ (x≈y ∷ᵣ d) = _ ∷ʳ _   , cong (_  ∷ʳ_) (proj₂
 
 -- From τ₁ ⊎ τ₂ = τ, compute the injection ι₂ such that τ₂ = ⊆-trans ι₂ τ.
 
-DisjointUnion-inj₂ : ∀ {xs ys zs xys : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} →
+DisjointUnion-inj₂ : ∀ {xys : List A} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : xys ⊆ zs} →
                       DisjointUnion τ₁ τ₂ τ → ∃ λ (ι₂ : ys ⊆ xys) → ⊆-trans ι₂ τ ≡ τ₂
 DisjointUnion-inj₂ []         = []       , refl
 DisjointUnion-inj₂ (y   ∷ₙ d) = _        , cong (y  ∷ʳ_) (proj₂ (DisjointUnion-inj₂ d))
@@ -220,8 +218,7 @@ DisjointUnion-inj₂ (x≈y ∷ₗ d) = _ ∷ʳ _   , cong (_  ∷ʳ_) (proj₂
 -- A sublist σ disjoint to both τ₁ and τ₂ is an equalizer
 -- for the separators of τ₁ and τ₂.
 
-equalize-separators : ∀ {us xs ys zs : List A}
-  {σ : us ⊆ zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} (let s = separateˡ τ₁ τ₂) →
+equalize-separators : ∀ {σ : ws ⊆ zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} (let s = separateˡ τ₁ τ₂) →
   Disjoint σ τ₁ → Disjoint σ τ₂ →
   ⊆-trans σ (Separation.separator₁ s) ≡
   ⊆-trans σ (Separation.separator₂ s)