    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An inductive definition of the sublist relation. This is commonly
    -- known as Order Preserving Embeddings (OPE).
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.List.Relation.Binary.Sublist.Propositional
      {a} {A : Set a} where

    open import Data.List.Base using (List)
    open import Data.List.Relation.Binary.Equality.Propositional using (≋⇒≡)
    import Data.List.Relation.Binary.Sublist.Setoid as SetoidSublist
    open import Data.List.Relation.Unary.Any using (Any)
    open import Relation.Binary.Core using (_⇒_)
    open import Relation.Binary.Bundles using (Preorder; Poset)
    open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder)
    open import Relation.Binary.Definitions using (Antisymmetric)
    open import Relation.Binary.PropositionalEquality.Core
      using (subst; _≡_; refl)
    open import Relation.Binary.PropositionalEquality.Properties
      using (setoid; isEquivalence)
    open import Relation.Unary using (Pred)

    ------------------------------------------------------------------------
    -- Re-export definition and operations from setoid sublists

    open SetoidSublist (setoid A) public
      hiding
      (lookup; ⊆-reflexive; ⊆-antisym
      ; ⊆-isPreorder; ⊆-isPartialOrder
      ; ⊆-preorder; ⊆-poset
      )

    ------------------------------------------------------------------------
    -- Additional operations

    module _ {p} {P : Pred A p} where

      lookup : ∀ {xs ys} → xs ⊆ ys → Any P xs → Any P ys
      lookup = SetoidSublist.lookup (setoid A) (subst _)

    ------------------------------------------------------------------------
    -- Relational properties

    ⊆-reflexive : _≡_ ⇒ _⊆_
    ⊆-reflexive refl = ⊆-refl

    ⊆-antisym : Antisymmetric _≡_ _⊆_
    ⊆-antisym xs⊆ys ys⊆xs = ≋⇒≡ (SetoidSublist.⊆-antisym (setoid A) xs⊆ys ys⊆xs)

    ⊆-isPreorder : IsPreorder _≡_ _⊆_
    ⊆-isPreorder = record
      { isEquivalence = isEquivalence
      ; reflexive     = ⊆-reflexive
      ; trans         = ⊆-trans
      }

    ⊆-isPartialOrder : IsPartialOrder _≡_ _⊆_
    ⊆-isPartialOrder = record
      { isPreorder = ⊆-isPreorder
      ; antisym    = ⊆-antisym
      }

    ⊆-preorder : Preorder a a a
    ⊆-preorder = record
      { isPreorder = ⊆-isPreorder
      }

    ⊆-poset : Poset a a a
    ⊆-poset = record
      { isPartialOrder = ⊆-isPartialOrder
      }

    ------------------------------------------------------------------------
    -- Separating two sublists
    --
    -- Two possibly overlapping sublists τ : xs ⊆ zs and σ : ys ⊆ zs
    -- can be turned into disjoint lists τρ : xs ⊆ zs and τρ : ys ⊆ zs′
    -- by duplicating all entries of zs that occur both in xs and ys,
    -- resulting in an extension ρ : zs ⊆ zs′ of zs.

    record Separation {xs ys zs} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) : Set a where
      field
        {inflation} : List A
        separator₁  : zs ⊆ inflation
        separator₂  : zs ⊆ inflation
      separated₁ = ⊆-trans τ₁ separator₁
      separated₂ = ⊆-trans τ₂ separator₂
      field
        disjoint    : Disjoint separated₁ separated₂

    infixr 5 _∷ₙ-Sep_ _∷ₗ-Sep_ _∷ᵣ-Sep_

    -- Empty separation

    []-Sep : Separation [] []
    []-Sep = record { separator₁ = [] ; separator₂ = [] ; disjoint = [] }

    -- Weaken a separation

    _∷ₙ-Sep_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
               ∀ z → Separation τ₁ τ₂ → Separation (z ∷ʳ τ₁) (z ∷ʳ τ₂)
    z ∷ₙ-Sep record{ separator₁ = ρ₁; separator₂ = ρ₂; disjoint = d } = record
      { separator₁ = refl ∷ ρ₁
      ; separator₂ = refl ∷ ρ₂
      ; disjoint   = z   ∷ₙ d
      }

    -- Extend a separation by an element of the first sublist.
    --
    -- Note: this requires a category law from the underlying equality,
    -- trans x=z refl = x=z, thus, separation is not available for Sublist.Setoid.

    _∷ₗ-Sep_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
              ∀ {x z} (x≡z : x ≡ z) → Separation τ₁ τ₂ → Separation (x≡z ∷ τ₁) (z ∷ʳ τ₂)
    refl ∷ₗ-Sep record{ separator₁ = ρ₁; separator₂ = ρ₂; disjoint = d } = record
      { separator₁ = refl ∷ ρ₁
      ; separator₂ = refl ∷ ρ₂
      ; disjoint   = refl ∷ₗ d
      }

    -- Extend a separation by an element of the second sublist.

    _∷ᵣ-Sep_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
              ∀ {y z} (y≡z : y ≡ z) → Separation τ₁ τ₂ → Separation (z ∷ʳ τ₁) (y≡z ∷ τ₂)
    refl ∷ᵣ-Sep record{ separator₁ = ρ₁; separator₂ = ρ₂; disjoint = d } = record
      { separator₁ = refl ∷ ρ₁
      ; separator₂ = refl ∷ ρ₂
      ; disjoint   = refl ∷ᵣ d
      }

    -- Extend a separation by a common element of both sublists.
    --
    -- Left-biased: the left separator gets the first copy
    -- of the common element.

    ∷-Sepˡ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
            ∀ {x y z} (x≡z : x ≡ z) (y≡z : y ≡ z) →
            Separation τ₁ τ₂ → Separation (x≡z ∷ τ₁) (y≡z ∷ τ₂)
    ∷-Sepˡ refl refl record{ separator₁ = ρ₁; separator₂ = ρ₂; disjoint = d } = record
      { separator₁ = _ ∷ʳ refl ∷ ρ₁
      ; separator₂ = refl ∷ _ ∷ʳ ρ₂
      ; disjoint   = refl ∷ᵣ (refl ∷ₗ d)
      }

    -- Left-biased separation of two sublists.  Of common elements,
    -- the first sublist receives the first copy.

    separateˡ : ∀ {xs ys zs} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Separation τ₁ τ₂
    separateˡ [] [] = []-Sep
    separateˡ (z  ∷ʳ τ₁) (z  ∷ʳ τ₂) = z   ∷ₙ-Sep separateˡ τ₁ τ₂
    separateˡ (z  ∷ʳ τ₁) (y≡z ∷ τ₂) = y≡z ∷ᵣ-Sep separateˡ τ₁ τ₂
    separateˡ (x≡z ∷ τ₁) (z  ∷ʳ τ₂) = x≡z ∷ₗ-Sep separateˡ τ₁ τ₂
    separateˡ (x≡z ∷ τ₁) (y≡z ∷ τ₂) = ∷-Sepˡ x≡z y≡z (separateˡ τ₁ τ₂)