------------------------------------------------------------------------
-- 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
open import Function.Base using (_$_; _∘_)
open import Level
open import Relation.Binary.HeterogeneousEquality.Core
open import Relation.Binary.PropositionalEquality.Core

------------------------------------------------------------------------
-- 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