    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An inductive definition of the heterogeneous infix relation
    ------------------------------------------------------------------------

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

    module Data.List.Relation.Binary.Infix.Heterogeneous where

    open import Level using (Level; _⊔_)
    open import Relation.Binary.Core using (REL; _⇒_)
    open import Data.List.Base as List using (List; []; _∷_; _++_)
    open import Data.List.Relation.Binary.Pointwise
      using (Pointwise)
    open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix
      using (Prefix; []; _∷_; _++ᵖ_)

    private
      variable
        a b r s : Level
        A : Set a
        B : Set b
        R : REL A B r
        S : REL A B s

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

      data Infix : REL (List A) (List B) (a ⊔ b ⊔ r) where
        here  : ∀ {as bs}   → Prefix R as bs → Infix as bs
        there : ∀ {b as bs} → Infix as bs → Infix as (b ∷ bs)

      data View (as : List A) : List B → Set (a ⊔ b ⊔ r) where
        MkView : ∀ pref {inf} → Pointwise R as inf → ∀ suff →
                View as (pref List.++ inf List.++ suff)

    infixr 5 _++ⁱ_ _ⁱ++_

    _++ⁱ_ : ∀ xs {as bs} → Infix R as bs → Infix R as (xs ++ bs)
    []       ++ⁱ rs = rs
    (x ∷ xs) ++ⁱ rs = there (xs ++ⁱ rs)

    _ⁱ++_ : ∀ {as bs} → Infix R as bs → ∀ xs → Infix R as (bs ++ xs)
    here  rs ⁱ++ xs = here (rs ++ᵖ xs)
    there rs ⁱ++ xs = there (rs ⁱ++ xs)

    map : R ⇒ S → Infix R ⇒ Infix S
    map R⇒S (here pref) = here (Prefix.map R⇒S pref)
    map R⇒S (there inf) = there (map R⇒S inf)

    toView : ∀ {as bs} → Infix R as bs → View R as bs
    toView (here p)  with inf Prefix.++ suff ← Prefix.toView p = MkView [] inf suff
    toView (there p) with MkView pref inf suff ← toView p      = MkView (_ ∷ pref) inf suff

    fromView : ∀ {as bs} → View R as bs → Infix R as bs
    fromView (MkView []         inf suff) = here (Prefix.fromView (inf Prefix.++ suff))
    fromView (MkView (a ∷ pref) inf suff) = there (fromView (MkView pref inf suff))