[ add ] lemma relating Propositional and Setoid versions of Sublist

CHANGELOG.md

@@ -317,6 +317,16 @@ Additions to existing modules
                                             ([] , [])
   ```
 
+* In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
+  ```agda
+  ⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs
+  ```
+
+* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
+  ```agda
+  ⊆ₚ⇒⊆ : as PropositionalSublist.⊆ bs → as ⊆ bs
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
@@ -397,6 +407,7 @@ Additions to existing modules
 * In `Data.List.Relation.Unary.All`:
   ```agda
   search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
+ ```
 
 * In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
   ```agda

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

@@ -16,11 +16,14 @@ open import Data.List.Relation.Unary.Any.Properties
   using (here-injective; there-injective)
 open import Data.List.Relation.Binary.Sublist.Propositional
   hiding (map)
+import Data.List.Relation.Binary.Sublist.Setoid
+  as SetoidSublist
 import Data.List.Relation.Binary.Sublist.Setoid.Properties
   as SetoidProperties
 open import Data.Product.Base using (∃; _,_; proj₂)
 open import Function.Base using (id; _∘_; _∘′_)
 open import Level using (Level)
+open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (_Respects_)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl; cong; _≗_; trans)
@@ -39,9 +42,24 @@ private
 -- Re-exporting setoid properties
 
 module _ {A : Set a} where
-  open SetoidProperties  (setoid A) public
+  open SetoidProperties (setoid A) public
     hiding (map⁺; ⊆-trans-idˡ; ⊆-trans-idʳ; ⊆-trans-assoc)
 
+------------------------------------------------------------------------
+-- Relationship between _⊆_ and Setoid._⊆_
+------------------------------------------------------------------------
+
+module _ (S : Setoid a ℓ) where
+
+  open Setoid S using (Carrier; _≈_; reflexive)
+  open SetoidSublist S using () renaming (_⊆_ to _⊆ₛ_)
+
+  ⊆⇒⊆ₛ : ∀ {as bs} → as ⊆ bs → as ⊆ₛ bs
+  ⊆⇒⊆ₛ = SetoidSublist.map (setoid Carrier) reflexive
+
+------------------------------------------------------------------------
+-- Functoriality of map
+
 map⁺ : (f : A → B) → xs ⊆ ys → map f xs ⊆ map f ys
 map⁺ f = SetoidProperties.map⁺ (setoid _) (setoid _) (cong f)
 

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

@@ -23,18 +23,20 @@ open import Function.Bundles using (_⇔_; _⤖_)
 open import Level
 open import Relation.Binary.Definitions using () renaming (Decidable to Decidable₂)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; cong; cong₂)
+open import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
 open import Relation.Binary.Structures using (IsDecTotalOrder)
 open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Decidable using (¬?; yes; no)
 
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
+import Data.List.Relation.Binary.Sublist.Propositional as PropositionalSublist
 import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
 import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
   as HeteroProperties
 import Data.List.Membership.Setoid as SetoidMembership
 
-open Setoid S using (_≈_; trans) renaming (Carrier to A; refl to ≈-refl)
+open Setoid S using (_≈_; trans; reflexive) renaming (Carrier to A; refl to ≈-refl)
 open SetoidEquality S using (_≋_; ≋-refl)
 open SetoidSublist S hiding (map)
 open SetoidMembership S using (_∈_)
@@ -66,6 +68,13 @@ module _ where
   ∷ʳ-injective : ∀ {pxs qxs : xs ⊆ ys} → y ∷ʳ pxs ≡ y ∷ʳ qxs → pxs ≡ qxs
   ∷ʳ-injective refl = refl
 
+------------------------------------------------------------------------
+-- Relationship between Propositional._⊆_ and _⊆_
+------------------------------------------------------------------------
+
+⊆ₚ⇒⊆ : as PropositionalSublist.⊆ bs → as ⊆ bs
+⊆ₚ⇒⊆ = SetoidSublist.map (setoid _) reflexive
+
 ------------------------------------------------------------------------
 -- Categorical properties
 ------------------------------------------------------------------------