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

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

    open import Data.List.Base using (List; []; _∷_; [_])
    open import Data.List.Relation.Unary.Any using (Any; here; there)
    open import Level using (_⊔_)
    open import Relation.Binary.Core using (REL; _⇒_)
    open import Relation.Binary.Definitions using (_⟶_Respects_; Min)
    open import Relation.Unary using (Pred)

    module Data.List.Relation.Binary.Sublist.Heterogeneous
      {a b r} {A : Set a} {B : Set b} {R : REL A B r}
      where

    ------------------------------------------------------------------------
    -- Re-export core definitions

    open import Data.List.Relation.Binary.Sublist.Heterogeneous.Core public

    ------------------------------------------------------------------------
    -- Type and basic combinators

    module _ {s} {S : REL A B s} where

      map : R ⇒ S → Sublist R ⇒ Sublist S
      map f []        = []
      map f (y ∷ʳ rs) = y ∷ʳ map f rs
      map f (r ∷ rs)  = f r ∷ map f rs

    minimum : Min (Sublist R) []
    minimum []       = []
    minimum (x ∷ xs) = x ∷ʳ minimum xs

    ------------------------------------------------------------------------
    -- Conversion to and from Any

    -- Special case: Sublist R [ a ] bs → Any (R a) bs
    toAny : ∀ {a as bs} → Sublist R (a ∷ as) bs → Any (R a) bs
    toAny (y ∷ʳ rs) = there (toAny rs)
    toAny (r ∷ rs)  = here r

    fromAny : ∀ {a bs} → Any (R a) bs → Sublist R [ a ] bs
    fromAny (here r)  = r ∷ minimum _
    fromAny (there p) = _ ∷ʳ fromAny p

    ------------------------------------------------------------------------
    -- Generalised lookup based on a proof of Any

    module _ {p q} {P : Pred A p} {Q : Pred B q} (resp : P ⟶ Q Respects R) where

      lookup : ∀ {xs ys} → Sublist R xs ys → Any P xs → Any Q ys
      lookup (y ∷ʳ p)  k         = there (lookup p k)
      lookup (rxy ∷ p) (here px) = here (resp rxy px)
      lookup (rxy ∷ p) (there k) = there (lookup p k)

    ------------------------------------------------------------------------
    -- Disjoint sublists xs,ys ⊆ zs
    --
    -- NB: This does not imply that xs and ys partition zs;
    -- zs may have additional elements.

    private
      infix 4 _⊆_
      _⊆_ = Sublist R

    infixr 5 _∷ₙ_ _∷ₗ_ _∷ᵣ_

    data Disjoint : ∀ {xs ys zs} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Set (a ⊔ b ⊔ r) where
      []   : Disjoint [] []

      -- Element y of zs is neither in xs nor in ys:
      _∷ₙ_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} →
             (y : B)       → Disjoint τ₁ τ₂ → Disjoint (y  ∷ʳ τ₁) (y  ∷ʳ τ₂)

      -- Element y of zs is in xs as x with x≈y:
      _∷ₗ_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {x y} →
             (x≈y : R x y) → Disjoint τ₁ τ₂ → Disjoint (x≈y ∷ τ₁) (y  ∷ʳ τ₂)

      -- Element y of zs is in ys as x with x≈y:
      _∷ᵣ_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {x y} →
             (x≈y : R x y) → Disjoint τ₁ τ₂ → Disjoint (y  ∷ʳ τ₁) (x≈y ∷ τ₂)

    ------------------------------------------------------------------------
    -- Disjoint union of two sublists xs,ys ⊆ zs
    --
    -- This is the Cover relation without overlap of Section 6 of
    -- Conor McBride, Everybody's Got To Be Somewhere,
    -- MSFP@FSCD 2018: 53-69.

    data DisjointUnion : ∀ {xs ys zs us} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) (τ : us ⊆ zs) →  Set (a ⊔ b ⊔ r) where
      []   : DisjointUnion [] [] []

      -- Element y of zs is neither in xs nor in ys: skip.
      _∷ₙ_ : ∀ {xs ys zs us} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : us ⊆ zs} →
             (y : B)       → DisjointUnion τ₁ τ₂ τ → DisjointUnion (y  ∷ʳ τ₁) (y  ∷ʳ τ₂) (y ∷ʳ τ)

      -- Element y of zs is in xs as x with x≈y: add to us.
      _∷ₗ_ : ∀ {xs ys zs us} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : us ⊆ zs} {x y} →
             (x≈y : R x y) → DisjointUnion τ₁ τ₂ τ → DisjointUnion (x≈y ∷ τ₁) (y  ∷ʳ τ₂) (x≈y ∷ τ)

      -- Element y of zs is in ys as x with x≈y: add to us.
      _∷ᵣ_ : ∀ {xs ys zs us} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : us ⊆ zs} {x y} →
             (x≈y : R x y) → DisjointUnion τ₁ τ₂ τ → DisjointUnion (y  ∷ʳ τ₁) (x≈y ∷ τ₂) (x≈y ∷ τ)