Source code on Github
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the heterogeneous suffix relation
------------------------------------------------------------------------

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

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

open import Level
open import Relation.Binary using (REL; _⇒_)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Binary.Pointwise as Pointwise
  using (Pointwise; []; _∷_)

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

  infixr 5 _++_

  data Suffix : REL (List A) (List B) (a  b  r) where
    here  :  {as bs}  Pointwise R as bs  Suffix as bs
    there :  {b as bs}  Suffix as bs  Suffix as (b  bs)

  data SuffixView (as : List A) : List B  Set (a  b  r) where
    _++_ :  cs {ds}  Pointwise R as ds  SuffixView as (cs List.++ ds)

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

  tail :  {a as bs}  Suffix R (a  as) bs  Suffix R as bs
  tail (here (_  rs)) = there (here rs)
  tail (there x) = there (tail x)

  _++ˢ_ :  pre {as bs}  Suffix R as bs  Suffix R as (pre List.++ bs)
  []       ++ˢ rs = rs
  (x  xs) ++ˢ rs = there (xs ++ˢ rs)

module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where

  map : R  S  Suffix R  Suffix S
  map R⇒S (here rs)   = here (Pointwise.map R⇒S rs)
  map R⇒S (there suf) = there (map R⇒S suf)

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

  toView :  {as bs}  Suffix R as bs  SuffixView R as bs
  toView (here rs) = [] ++ rs
  toView (there {c} suf) with toView suf
  ... | cs ++ rs = (c  cs) ++ rs

  fromView :  {as bs}  SuffixView R as bs  Suffix R as bs
  fromView ([]       ++ rs) = here rs
  fromView ((c  cs) ++ rs) = there (fromView (cs ++ rs))