    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Generalised notion of interleaving two lists into one in an
    -- order-preserving manner
    ------------------------------------------------------------------------

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

    module Data.List.Relation.Ternary.Interleaving where

    open import 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 as Product using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂)
    open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
    open import Function.Base
    open import Relation.Binary.Core using (REL; _⇒_)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

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

    module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
             (L : REL A C l) (R : REL B C r) where

      infixr 5 _∷ˡ_ _∷ʳ_

      data Interleaving : List A → List B → List C → Set (a ⊔ b ⊔ c ⊔ l ⊔ r) where
        []   : Interleaving [] [] []
        _∷ˡ_ : ∀ {a c l r cs} → L a c → Interleaving l r cs → Interleaving (a ∷ l) r (c ∷ cs)
        _∷ʳ_ : ∀ {b c l r cs} → R b c → Interleaving l r cs → Interleaving l (b ∷ r) (c ∷ cs)

    ------------------------------------------------------------------------
    -- Operations

    module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
             {L : REL A C l} {R : REL B C r} where

    -- injections

      left : ∀ {as cs} → Pointwise L as cs → Interleaving L R as [] cs
      left []       = []
      left (l ∷ pw) = l ∷ˡ left pw

      right : ∀ {bs cs} → Pointwise R bs cs → Interleaving L R [] bs cs
      right []       = []
      right (r ∷ pw) = r ∷ʳ right pw

    -- swap

      swap : ∀ {cs l r} → Interleaving L R l r cs → Interleaving R L r l cs
      swap []        = []
      swap (l ∷ˡ sp) = l ∷ʳ swap sp
      swap (r ∷ʳ sp) = r ∷ˡ swap sp

    -- extract the "proper" equality split from the pointwise relations

      break : ∀ {cs l r} → Interleaving L R l r cs → ∃ $ uncurry $ λ csl csr →
              Interleaving _≡_ _≡_ csl csr cs × Pointwise L l csl × Pointwise R r csr
      break []        = -, [] , [] , []
      break (l ∷ˡ sp) = let (_ , eq , pwl , pwr) = break sp in
                        -, refl ∷ˡ eq , l ∷ pwl , pwr
      break (r ∷ʳ sp) = let (_ , eq , pwl , pwr) = break sp in
                        -, refl ∷ʳ eq , pwl , r ∷ pwr

    -- map

    module _ {a b c l r p q} {A : Set a} {B : Set b} {C : Set c}
             {L : REL A C l} {R : REL B C r} {P : REL A C p} {Q : REL B C q} where

      map : ∀ {cs l r} → L ⇒ P → R ⇒ Q → Interleaving L R l r cs → Interleaving P Q l r cs
      map L⇒P R⇒Q []        = []
      map L⇒P R⇒Q (l ∷ˡ sp) = L⇒P l ∷ˡ map L⇒P R⇒Q sp
      map L⇒P R⇒Q (r ∷ʳ sp) = R⇒Q r ∷ʳ map L⇒P R⇒Q sp

    module _ {a b c l r p} {A : Set a} {B : Set b} {C : Set c}
             {L : REL A C l} {R : REL B C r} where

      map₁ : ∀ {P : REL A C p} {as l r} → L ⇒ P →
             Interleaving L R l r as → Interleaving P R l r as
      map₁ L⇒P = map L⇒P id

      map₂ : ∀ {P : REL B C p} {as l r} → R ⇒ P →
             Interleaving L R l r as → Interleaving L P l r as
      map₂ = map id

    ------------------------------------------------------------------------
    -- Special case: The second and third list have the same type

    module _ {a b l r} {A : Set a} {B : Set b} {L : REL A B l} {R : REL A B r} where

    -- converting back and forth with pointwise

      split : ∀ {as bs} → Pointwise (λ a b → L a b ⊎ R a b) as bs →
              ∃₂ λ asr asl → Interleaving L R asl asr bs
      split []            = [] , [] , []
      split (inj₁ l ∷ pw) = Product.map _ (Product.map _ (l ∷ˡ_)) (split pw)
      split (inj₂ r ∷ pw) = Product.map _ (Product.map _ (r ∷ʳ_)) (split pw)

      unsplit : ∀ {l r as} → Interleaving L R l r as →
                ∃ λ bs → Pointwise (λ a b → L a b ⊎ R a b) bs as
      unsplit []        = -, []
      unsplit (l ∷ˡ sp) = Product.map _ (inj₁ l ∷_) (unsplit sp)
      unsplit (r ∷ʳ sp) = Product.map _ (inj₂ r ∷_) (unsplit sp)