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

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

    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Bundles using (Setoid)

    module Data.List.Relation.Binary.Sublist.Setoid
      {c ℓ} (S : Setoid c ℓ) where

    open import Level using (_⊔_)

    open import Data.List.Base using (List; []; _∷_)
    import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
    import Data.List.Relation.Binary.Sublist.Heterogeneous as Heterogeneous
    import Data.List.Relation.Binary.Sublist.Heterogeneous.Core
      as HeterogeneousCore
    import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
      as HeterogeneousProperties
    open import Data.Product.Base using (∃; ∃₂; _×_; _,_; proj₂)

    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.PropositionalEquality.Core as ≡ using (_≡_)
    open import Relation.Nullary using (¬_; Dec; yes; no)

    open Setoid S renaming (Carrier to A)
    open SetoidEquality S

    ------------------------------------------------------------------------
    -- Definition

    infix 4 _⊆_ _⊇_ _⊂_ _⊃_ _⊈_ _⊉_ _⊄_ _⊅_

    _⊆_ : Rel (List A) (c ⊔ ℓ)
    _⊆_ = Heterogeneous.Sublist _≈_

    _⊇_ : Rel (List A) (c ⊔ ℓ)
    xs ⊇ ys = ys ⊆ xs

    _⊂_ : Rel (List A) (c ⊔ ℓ)
    xs ⊂ ys = xs ⊆ ys × ¬ (xs ≋ ys)

    _⊃_ : Rel (List A) (c ⊔ ℓ)
    xs ⊃ ys = ys ⊂ xs

    _⊈_ : Rel (List A) (c ⊔ ℓ)
    xs ⊈ ys = ¬ (xs ⊆ ys)

    _⊉_ : Rel (List A) (c ⊔ ℓ)
    xs ⊉ ys = ¬ (xs ⊇ ys)

    _⊄_ : Rel (List A) (c ⊔ ℓ)
    xs ⊄ ys = ¬ (xs ⊂ ys)

    _⊅_ : Rel (List A) (c ⊔ ℓ)
    xs ⊅ ys = ¬ (xs ⊃ ys)

    ------------------------------------------------------------------------
    -- Re-export definitions and operations from heterogeneous sublists

    open HeterogeneousCore _≈_ public
      using ([]; _∷_; _∷ʳ_)

    open Heterogeneous {R = _≈_} public
      hiding (Sublist; []; _∷_; _∷ʳ_)
      renaming
      ( toAny   to to∈
      ; fromAny to from∈
      )

    open Disjoint public
      using ([])

    open DisjointUnion public
      using ([])

    ------------------------------------------------------------------------
    -- Relational properties holding for Setoid case

    ⊆-reflexive : _≋_ ⇒ _⊆_
    ⊆-reflexive = HeterogeneousProperties.fromPointwise

    open HeterogeneousProperties.Reflexivity {R = _≈_} refl public using ()
      renaming (refl to ⊆-refl)  -- ⊆-refl : Reflexive _⊆_

    open HeterogeneousProperties.Transitivity {R = _≈_} {S = _≈_} {T = _≈_} trans public using ()
      renaming (trans to ⊆-trans)  -- ⊆-trans : Transitive _⊆_

    open HeterogeneousProperties.Antisymmetry {R = _≈_} {S = _≈_} (λ x≈y _ → x≈y) public using ()
      renaming (antisym to ⊆-antisym)  -- ⊆-antisym : Antisymmetric _≋_ _⊆_

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

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

    ⊆-preorder : Preorder c (c ⊔ ℓ) (c ⊔ ℓ)
    ⊆-preorder = record
      { isPreorder = ⊆-isPreorder
      }

    ⊆-poset : Poset c (c ⊔ ℓ) (c ⊔ ℓ)
    ⊆-poset = record
      { isPartialOrder = ⊆-isPartialOrder
      }

    ------------------------------------------------------------------------
    -- Raw pushout
    --
    -- The category _⊆_ does not have proper pushouts.  For instance consider:
    --
    --   τᵤ : [] ⊆ (u ∷ [])
    --   τᵥ : [] ⊆ (v ∷ [])
    --
    -- Then, there are two unrelated upper bounds (u ∷ v ∷ []) and (v ∷ u ∷ []),
    -- since _⊆_ does not include permutations.
    --
    -- Even though there are no unique least upper bounds, we can merge two
    -- extensions of a list, producing a minimial superlist of both.
    --
    -- For the example, the left-biased merge would produce the pair:
    --
    --   τᵤ′ : (u ∷ []) ⊆ (u ∷ v ∷ [])
    --   τᵥ′ : (v ∷ []) ⊆ (u ∷ v ∷ [])
    --
    -- We call such a pair a raw pushout.  It is then a weak pushout if the
    -- resulting square commutes, i.e.:
    --
    --   ⊆-trans τᵤ τᵤ′ ~ ⊆-trans τᵥ τᵥ′
    --
    -- This requires a notion of equality _~_ on sublist morphisms.
    --
    -- Further, commutation requires a similar commutation property
    -- for the underlying equality _≈_, namely
    --
    --   trans x≈y (sym x≈y) == trans x≈z (sym x≈z)
    --
    -- for some notion of equality _==_ for equality proofs _≈_.
    -- Such a property is given e.g. if _≈_ is proof irrelevant
    -- or forms a groupoid.

    record RawPushout {xs ys zs : List A} (τ : xs ⊆ ys) (σ : xs ⊆ zs) : Set (c ⊔ ℓ) where
      field
        {upperBound} : List A
        leg₁         : ys ⊆ upperBound
        leg₂         : zs ⊆ upperBound

    open RawPushout using (leg₁; leg₂)

    ------------------------------------------------------------------------
    -- Extending corners of a raw pushout square

    -- Extending the right upper corner.

    infixr 5 _∷ʳ₁_ _∷ʳ₂_

    _∷ʳ₁_ : ∀ {xs ys zs : List A} {τ : xs ⊆ ys} {σ : xs ⊆ zs} →
            (y : A) → RawPushout τ σ → RawPushout (y ∷ʳ τ) σ
    y ∷ʳ₁ rpo = record
      { leg₁ = refl ∷ leg₁ rpo
      ; leg₂ = y   ∷ʳ leg₂ rpo
      }

    -- Extending the left lower corner.

    _∷ʳ₂_ : ∀ {xs ys zs : List A} {τ : xs ⊆ ys} {σ : xs ⊆ zs} →
            (z : A) → RawPushout τ σ → RawPushout τ (z ∷ʳ σ)
    z ∷ʳ₂ rpo = record
      { leg₁ = z   ∷ʳ leg₁ rpo
      ; leg₂ = refl ∷ leg₂ rpo
      }

    -- Extending both of these corners with equal elements.

    ∷-rpo : ∀ {x y z : A} {xs ys zs : List A} {τ : xs ⊆ ys} {σ : xs ⊆ zs} →
            (x≈y : x ≈ y) (x≈z : x ≈ z) → RawPushout τ σ → RawPushout (x≈y ∷ τ) (x≈z ∷ σ)
    ∷-rpo x≈y x≈z rpo = record
      { leg₁ = sym x≈y ∷ leg₁ rpo
      ; leg₂ = sym x≈z ∷ leg₂ rpo
      }

    ------------------------------------------------------------------------
    -- Left-biased pushout: add elements of left extension first.

    ⊆-pushoutˡ : ∀ {xs ys zs : List A} →
                 (τ : xs ⊆ ys) (σ : xs ⊆ zs) → RawPushout τ σ
    ⊆-pushoutˡ []        σ         = record { leg₁ = σ ; leg₂ = ⊆-refl }
    ⊆-pushoutˡ (y  ∷ʳ τ) σ         = y ∷ʳ₁ ⊆-pushoutˡ τ σ
    ⊆-pushoutˡ τ@(_ ∷ _) (z  ∷ʳ σ) = z ∷ʳ₂ ⊆-pushoutˡ τ σ
    ⊆-pushoutˡ (x≈y ∷ τ) (x≈z ∷ σ) = ∷-rpo x≈y x≈z (⊆-pushoutˡ τ σ)

    -- Join two extensions, returning the upper bound and the diagonal
    -- of the pushout square.

    ⊆-joinˡ : ∀ {xs ys zs : List A} →
              (τ : xs ⊆ ys) (σ : xs ⊆ zs) → ∃ λ us → xs ⊆ us
    ⊆-joinˡ τ σ = RawPushout.upperBound rpo , ⊆-trans τ (leg₁ rpo)
      where
      rpo = ⊆-pushoutˡ τ σ

    ------------------------------------------------------------------------
    -- Upper bound of two sublists xs,ys ⊆ zs
    --
    -- Two sublists τ : xs ⊆ zs and σ : ys ⊆ zs
    -- can be joined in a unique way if τ and σ are respected.
    --
    -- For instance, if τ : [x] ⊆ [x,y,x] and σ : [y] ⊆ [x,y,x]
    -- then the union will be [x,y] or [y,x], depending on whether
    -- τ picks the first x or the second one.
    --
    -- NB: If the content of τ and σ were ignored then the union would not
    -- be unique.  Expressing uniqueness would require a notion of equality
    -- of sublist proofs, which we do not (yet) have for the setoid case
    -- (however, for the propositional case).

    record UpperBound {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) : Set (c ⊔ ℓ) where
      field
        {theUpperBound} : List A
        sub  : theUpperBound ⊆ zs
        inj₁ : xs ⊆ theUpperBound
        inj₂ : ys ⊆ theUpperBound

    open UpperBound

    infixr 5 _∷ₗ-ub_ _∷ᵣ-ub_

    ∷ₙ-ub : ∀ {xs ys zs} {τ : xs ⊆ zs} {σ : ys ⊆ zs} {x} →
            UpperBound τ σ → UpperBound (x ∷ʳ τ) (x ∷ʳ σ)
    ∷ₙ-ub u = record
      { sub  = _ ∷ʳ u .sub
      ; inj₁ = u .inj₁
      ; inj₂ = u .inj₂
      }

    _∷ₗ-ub_ : ∀ {xs ys zs} {τ : xs ⊆ zs} {σ : ys ⊆ zs} {x y} →
             (x≈y : x ≈ y) → UpperBound τ σ → UpperBound (x≈y ∷ τ) (y ∷ʳ σ)
    x≈y ∷ₗ-ub u = record
      { sub = refl ∷ u .sub
      ; inj₁ = x≈y ∷ u .inj₁
      ; inj₂ = _  ∷ʳ u .inj₂
      }

    _∷ᵣ-ub_ : ∀ {xs ys zs} {τ : xs ⊆ zs} {σ : ys ⊆ zs} {x y} →
             (x≈y : x ≈ y) → UpperBound τ σ → UpperBound (y ∷ʳ τ) (x≈y ∷ σ)
    x≈y ∷ᵣ-ub u = record
      { sub  = refl ∷ u .sub
      ; inj₁ = _   ∷ʳ u .inj₁
      ; inj₂ = x≈y  ∷ u .inj₂
      }

    _,_∷-ub_ : ∀ {xs ys zs} {τ : xs ⊆ zs} {σ : ys ⊆ zs} {x y z} →
             (x≈z : x ≈ z) (y≈z : y ≈ z) → UpperBound τ σ → UpperBound (x≈z ∷ τ) (y≈z ∷ σ)
    x≈z , y≈z ∷-ub u = record
      { sub  =  refl ∷ u .sub
      ; inj₁ =  x≈z  ∷ u .inj₁
      ; inj₂ =  y≈z  ∷ u .inj₂
      }

    ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ
    ⊆-upper-bound []        []        = record { sub = [] ; inj₁ = [] ; inj₂ = [] }
    ⊆-upper-bound (y ∷ʳ τ)  (.y ∷ʳ σ) = ∷ₙ-ub (⊆-upper-bound τ σ)
    ⊆-upper-bound (y ∷ʳ τ)  (x≈y ∷ σ) = x≈y ∷ᵣ-ub ⊆-upper-bound τ σ
    ⊆-upper-bound (x≈y ∷ τ) (y  ∷ʳ σ) = x≈y ∷ₗ-ub ⊆-upper-bound τ σ
    ⊆-upper-bound (x≈z ∷ τ) (y≈z ∷ σ) = x≈z , y≈z ∷-ub ⊆-upper-bound τ σ

    ------------------------------------------------------------------------
    -- Disjoint union
    --
    -- Upper bound of two non-overlapping sublists.

    ⊆-disjoint-union : ∀ {xs ys zs} {τ : xs ⊆ zs} {σ : ys ⊆ zs} →
                       Disjoint τ σ → UpperBound τ σ
    ⊆-disjoint-union {τ = τ} {σ = σ} _ = ⊆-upper-bound τ σ