------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of pointwise equality for containers
------------------------------------------------------------------------

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

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

open import Axiom.Extensionality.Propositional using (Extensionality)
open import Data.Container.Core using (Container; ⟦_⟧)
open import Data.Container.Relation.Binary.Pointwise
  using (Pointwise; _,_)
open import Data.Product.Base using (_,_; Σ-syntax; -,_)
open import Level using (_⊔_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions
  using (Reflexive; Symmetric; Transitive)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core as 
  using (_≡_; subst; cong)

module _ {s p x r} {X : Set x} (C : Container s p) (R : Rel X r) where

  refl : Reflexive R  Reflexive (Pointwise C R)
  refl R-refl = ≡.refl , λ p  R-refl

  sym : Symmetric R  Symmetric (Pointwise C R)
  sym R-sym (≡.refl , f) = ≡.refl , λ p  R-sym (f p)

  trans : Transitive R  Transitive (Pointwise C R)
  trans R-trans (≡.refl , f) (≡.refl , g) = ≡.refl , λ p  R-trans (f p) (g p)

private

  -- Note that, if propositional equality were extensional, then
  -- Eq _≡_ and _≡_ would coincide.

  Eq⇒≡ :  {s p x} {C : Container s p} {X : Set x} {xs ys :  C  X} 
         Extensionality p x  Pointwise C _≡_ xs ys  xs  ys
  Eq⇒≡ ext (≡.refl , f≈f′) = cong -,_ (ext f≈f′)