    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Results concerning function extensionality for propositional equality
    ------------------------------------------------------------------------

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

    module Axiom.Extensionality.Heterogeneous where

    import Axiom.Extensionality.Propositional as P
      using (Extensionality; lower-extensionality)
    open import Function.Base using (_$_; _∘_)
    open import Level using (Level; suc)
    open import Relation.Binary.HeterogeneousEquality.Core
      using (_≅_; ≅-to-≡; ≡-to-≅)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

    ------------------------------------------------------------------------
    -- Function extensionality states that if two functions are
    -- propositionally equal for every input, then the functions themselves
    -- must be propositionally equal.

    Extensionality : (a b : Level) → Set _
    Extensionality a b =
      {A : Set a} {B₁ B₂ : A → Set b}
      {f₁ : (x : A) → B₁ x} {f₂ : (x : A) → B₂ x} →
      (∀ x → B₁ x ≡ B₂ x) → (∀ x → f₁ x ≅ f₂ x) → f₁ ≅ f₂

    ------------------------------------------------------------------------
    -- Properties

    -- This form of extensionality follows from extensionality for _≡_.

    ≡-ext⇒≅-ext : ∀ {ℓ₁ ℓ₂} →
                  P.Extensionality ℓ₁ (suc ℓ₂) →
                  Extensionality ℓ₁ ℓ₂
    ≡-ext⇒≅-ext {ℓ₁} {ℓ₂} ext B₁≡B₂ f₁≅f₂ with ext B₁≡B₂
    ... | refl = ≡-to-≅ $ ext′ (≅-to-≡ ∘ f₁≅f₂)
      where
      ext′ : P.Extensionality ℓ₁ ℓ₂
      ext′ = P.lower-extensionality ℓ₁ (suc ℓ₂) ext