1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465-------------------------------------------------------------------------- The Agda standard library---- Pointwise lifting of relations to lists------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.List.Relation.Binary.Pointwise.Base where open import Data.Product.Base as Product using (_×_; _,_; <_,_>; ∃-syntax)open import Data.List.Base using (List; []; _∷_)open import Level using (Level; _⊔_)open import Relation.Binary.Core using (REL; _⇒_)open import Relation.Binary.Construct.Composition using (_;_) private variable a b c ℓ : Level A B : Set a x y : A xs ys : List A R S : REL A B ℓ -------------------------------------------------------------------------- Definition------------------------------------------------------------------------ infixr 5 _∷_ data Pointwise {A : Set a} {B : Set b} (R : REL A B ℓ) : List A → List B → Set (a ⊔ b ⊔ ℓ) where [] : Pointwise R [] [] _∷_ : (x∼y : R x y) (xs∼ys : Pointwise R xs ys) → Pointwise R (x ∷ xs) (y ∷ ys) -------------------------------------------------------------------------- Operations------------------------------------------------------------------------ head : Pointwise R (x ∷ xs) (y ∷ ys) → R x yhead (x∼y ∷ xs∼ys) = x∼y tail : Pointwise R (x ∷ xs) (y ∷ ys) → Pointwise R xs ystail (x∼y ∷ xs∼ys) = xs∼ys uncons : Pointwise R (x ∷ xs) (y ∷ ys) → R x y × Pointwise R xs ysuncons = < head , tail > rec : ∀ (P : ∀ {xs ys} → Pointwise R xs ys → Set c) → (∀ {x y xs ys} {Rxsys : Pointwise R xs ys} → (Rxy : R x y) → P Rxsys → P (Rxy ∷ Rxsys)) → P [] → ∀ {xs ys} (Rxsys : Pointwise R xs ys) → P Rxsysrec P c n [] = nrec P c n (Rxy ∷ Rxsys) = c Rxy (rec P c n Rxsys) map : R ⇒ S → Pointwise R ⇒ Pointwise Smap R⇒S [] = []map R⇒S (Rxy ∷ Rxsys) = R⇒S Rxy ∷ map R⇒S Rxsys unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S)unzip [] = [] , [] , []unzip ((y , r , s) ∷ xs∼ys) = Product.map (y ∷_) (Product.map (r ∷_) (s ∷_)) (unzip xs∼ys)