------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise equality for indexed containers
------------------------------------------------------------------------

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

module Data.Container.Indexed.Relation.Binary.Pointwise where

open import Data.Product.Base using (_,_; Σ-syntax)
open import Data.Container.Indexed.Core using (Container; Subtrees; ⟦_⟧)
open import Function.Base using (_∘_)
open import Level using (Level; _⊔_)
open import Relation.Binary using (REL; _⇒_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

private variable
  ℓᵉ ℓᵉ′ ℓᵖ ℓˢ ℓˣ ℓʸ : Level
  I O : Set _

------------------------------------------------------------------------
-- Equality, parametrised on an underlying relation.

-- Since ⟦_⟧ is a Σ-type, not a record, I'd say Pointwise should also be
-- a Σ-type, not a record. Maybe we need to update module
-- `Data.Container.Relation.Binary.Pointwise` accordingly...
--
-- record Pointwise  : Set (ℓˢ ⊔ ℓᵖ ⊔ ℓᵉ) where
--   constructor _,_
--   field shape    : c ≡ c'
--         position : Eqs shape xs ys

module _ (C : Container I O ℓˢ ℓᵖ)
         {X : I → Set ℓˣ} {Y : I → Set ℓʸ} (R : (i : I) → REL (X i) (Y i) ℓᵉ)
         (o : O)
         ((c  , xs) : ⟦ C ⟧ X o)
         ((c' , ys) : ⟦ C ⟧ Y o)
  where
  open Container C

  Eqs : c ≡ c' → Subtrees C X o c → Subtrees C Y o c' → Set _
  Eqs refl xs ys = (r : Response c) → R (next c r) (xs r) (ys r)

  Pointwise = Σ[ eq ∈ c ≡ c' ] Eqs eq xs ys

------------------------------------------------------------------------
-- Operations

module _ {C : Container I O ℓˢ ℓᵖ}
         {X : I → Set ℓˣ} {Y : I → Set ℓʸ}
         {R  : (i : I) → REL (X i) (Y i) ℓᵉ}
         {R′ : (i : I) → REL (X i) (Y i) ℓᵉ′}
         where

  map : (R⇒R′ : ∀ i → R i ⇒ R′ i) {o : O} → Pointwise C R o ⇒ Pointwise C R′ o
  map R⇒R′ (refl , f) = refl , R⇒R′ _ ∘ f