```------------------------------------------------------------------------
-- 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))
```