    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of the generalised view of appending two lists
    ------------------------------------------------------------------------

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

    module Data.List.Relation.Ternary.Appending.Properties where

    open import Data.List.Base using (List; [])
    open import Data.List.Relation.Ternary.Appending
    open import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise; []; _∷_)
    open import Data.Product.Base as Product using (∃-syntax; _×_; _,_)
    open import Function.Base using (id)
    open import Data.List.Relation.Binary.Pointwise.Base as Pw using (Pointwise; []; _∷_)
    open import Data.List.Relation.Binary.Pointwise.Properties as Pw using (transitive)
    open import Level using (Level)
    open import Relation.Binary.Core using (REL; Rel; _⇒_)
    open import Relation.Binary.Definitions using (Trans)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
    open import Relation.Binary.Construct.Composition using (_;_)

    private
      variable
        a ℓ l r : Level
        A A′ B B′ C C′ D D′ : Set a
        R S T U V W X Y : REL A B ℓ
        as bs cs ds : List A

    module _  (RST : Trans R S T) (USV : Trans U S V) where

      respʳ-≋ : Appending R U as bs cs → Pointwise S cs ds → Appending T V as bs ds
      respʳ-≋ ([]++ rs) es       = []++ Pw.transitive USV rs es
      respʳ-≋ (l ∷ lrs) (e ∷ es) = RST l e ∷ respʳ-≋ lrs es

    module _  {T : REL A B l} (RST : Trans R S T)
              {W : REL A B r} (ERW : Trans U V W)
              where

      respˡ-≋ : ∀ {as′ bs′} → Pointwise R as′ as → Pointwise U bs′ bs →
                Appending S V as bs cs → Appending T W as′ bs′ cs
      respˡ-≋ []         esʳ ([]++ rs) = []++ Pw.transitive ERW esʳ rs
      respˡ-≋ (eˡ ∷ esˡ) esʳ (l ∷ lrs) = RST eˡ l ∷ respˡ-≋ esˡ esʳ lrs

    conicalˡ : Appending R S as bs [] → as ≡ []
    conicalˡ ([]++ rs) = refl

    conicalʳ : Appending R S as bs [] → bs ≡ []
    conicalʳ ([]++ []) = refl

    through→ :
      (R ⇒ (S ; T)) →
      ((U ; V) ⇒ (W ; T)) →
      ∃[ xs ] Pointwise U as xs × Appending V R xs bs cs →
      ∃[ ys ] Appending W S as bs ys × Pointwise T ys cs
    through→ f g (_ , [] , []++ rs) =
      let _ , rs′ , ps′ = Pw.unzip (Pw.map f rs) in
      _ , []++ rs′ , ps′
    through→ f g (_ , p ∷ ps , l ∷ lrs) =
      let _ , l′ , p′ = g (_ , p , l) in
      Product.map _ (Product.map (l′ ∷_) (p′ ∷_)) (through→ f g (_ , ps , lrs))

    through← :
      ((R ; S) ⇒ T) →
      ((U ; S) ⇒ (V ; W)) →
      ∃[ ys ] Appending U R as bs ys × Pointwise S ys cs →
      ∃[ xs ] Pointwise V as xs × Appending W T xs bs cs
    through← f g (_ , []++ rs′ , ps′) =
      _ , [] , []++ (Pw.transitive (λ r′ p′ → f (_ , r′ , p′)) rs′ ps′)
    through← f g (_ , l′ ∷ lrs′ , p′ ∷ ps′) =
      let _ , p , l = g (_ , l′ , p′) in
      Product.map _ (Product.map (p ∷_) (l ∷_)) (through← f g (_ , lrs′ , ps′))

    assoc→ :
      (R ⇒ (S ; T)) →
      ((U ; V) ⇒ (W ; T)) →
      ((Y ; V) ⇒ X) →
      ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds →
      ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds
    assoc→ f g h (_ , []++ rs , lrs′) =
      let _ , mss , ss′ = through→ f g (_ , rs , lrs′) in
      _ , mss , []++ ss′
    assoc→ f g h (_ , l ∷ lrs , l′ ∷ lrs′) =
      Product.map₂ (Product.map₂ (h (_ , l , l′) ∷_)) (assoc→ f g h (_ , lrs , lrs′))

    assoc← :
      ((S ; T) ⇒ R) →
      ((W ; T) ⇒ (U ; V)) →
      (X ⇒ (Y ; V)) →
      ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds →
      ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds
    assoc← f g h (_ , mss , []++ ss′) =
      let _ , rs , lrs′ = through← f g (_ , mss , ss′) in
      _ , []++ rs , lrs′
    assoc← f g h (_ , mss , m′ ∷ mss′) =
      let _ , l , l′ = h m′ in
      Product.map _ (Product.map (l ∷_) (l′ ∷_)) (assoc← f g h (_ , mss , mss′))