    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Generalised view of appending two lists into one.
    ------------------------------------------------------------------------

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

    module Data.List.Relation.Ternary.Appending {a b c} {A : Set a} {B : Set b} {C : Set c} where

    open import Level using (Level; _⊔_)
    open import Data.List.Base as List using (List; []; _∷_)
    open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
    open import Data.Product.Base using (∃₂; _×_; _,_; -,_)
    open import Relation.Binary.Core using (REL)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

    private
      variable
        l r : Level
        L : REL A C l
        R : REL B C r
        as : List A
        bs : List B
        cs : List C

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

    module _ (L : REL A C l) (R : REL B C r) where

      infixr 5 _∷_ []++_

      data Appending : List A → List B → List C → Set (a ⊔ b ⊔ c ⊔ l ⊔ r) where
        []++_  : ∀ {bs cs} → Pointwise R bs cs → Appending [] bs cs
        _∷_    : ∀ {a as bs c cs} → L a c → Appending as bs cs → Appending (a ∷ as) bs (c ∷ cs)

    ------------------------------------------------------------------------
    -- Functions manipulating Appending

    infixr 5 _++_

    _++_ : ∀ {cs₁ cs₂ : List C} → Pointwise L as cs₁ → Pointwise R bs cs₂ →
           Appending L R as bs (cs₁ List.++ cs₂)
    []       ++ rs = []++ rs
    (l ∷ ls) ++ rs = l ∷ (ls ++ rs)

    -- extract the "proper" equality split from the pointwise relation
    break : Appending L R as bs cs → ∃₂ λ cs₁ cs₂ →
            cs₁ List.++ cs₂ ≡ cs × Pointwise L as cs₁ × Pointwise R bs cs₂
    break ([]++ rs) = -, -, (refl , [] , rs)
    break (l ∷ lrs) =
      let (_ , _ , eq , ls , rs) = break lrs in
      -, -, (cong (_ ∷_) eq , l ∷ ls , rs)