    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties that are related to pointwise lifting of binary
    -- relations to sigma types and make use of heterogeneous equality
    ------------------------------------------------------------------------

    {-# OPTIONS --with-K --safe #-}

    module Data.Product.Relation.Binary.Pointwise.Dependent.WithK where

    open import Data.Product.Base using (Σ; uncurry; _,_)
    open import Data.Product.Relation.Binary.Pointwise.Dependent
    open import Function.Base using (id)
    open import Function.Bundles using (Inverse)
    open import Level using (Level)
    open import Relation.Binary.Core using (_⇒_)
    open import Relation.Binary.HeterogeneousEquality as ≅ using (_≅_)
    open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid)
    open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
    import Relation.Binary.PropositionalEquality.Properties as ≡

    private
      variable
        a b : Level
        I : Set a
        A : I → Set a

    ------------------------------------------------------------------------
    -- The propositional equality setoid over sigma types can be
    -- decomposed using Pointwise

    Pointwise-≡⇒≡ : Pointwise A _≡_ (λ x y → x ≅ y) ⇒ _≡_
    Pointwise-≡⇒≡ (≡.refl , ≅.refl) = ≡.refl

    ≡⇒Pointwise-≡ : _≡_ ⇒ Pointwise A _≡_ (λ x y → x ≅ y)
    ≡⇒Pointwise-≡ ≡.refl = (≡.refl , ≅.refl)

    Pointwise-≡↔≡ : Inverse (setoid (≡.setoid I) (≅.indexedSetoid A)) (≡.setoid (Σ I A))
    Pointwise-≡↔≡ = record
      { to         = id
      ; to-cong    = Pointwise-≡⇒≡
      ; from       = id
      ; from-cong  = ≡⇒Pointwise-≡
      ; inverse    = (λ {(≡.refl , ≅.refl) → ≡.refl}) , λ {≡.refl → (≡.refl , ≅.refl)}
      }