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

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

    module Axiom.Extensionality.Propositional where

    open import Function.Base
    open import Level using (Level; _⊔_; suc; lift)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

    ------------------------------------------------------------------------
    -- 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 : A → Set b} {f g : (x : A) → B x} →
      (∀ x → f x ≡ g x) → f ≡ g

    -- A variant for implicit function spaces.

    ExtensionalityImplicit : (a b : Level) → Set _
    ExtensionalityImplicit a b =
      {A : Set a} {B : A → Set b} {f g : {x : A} → B x} →
      (∀ {x} → f {x} ≡ g {x}) → (λ {x} → f {x}) ≡ (λ {x} → g {x})

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

    -- If extensionality holds for a given universe level, then it also
    -- holds for lower ones.

    lower-extensionality : ∀ {a₁ b₁} a₂ b₂ →
                           Extensionality (a₁ ⊔ a₂) (b₁ ⊔ b₂) →
                           Extensionality a₁ b₁
    lower-extensionality a₂ b₂ ext f≡g = cong (λ h → Level.lower ∘ h ∘ lift) $
        ext (cong (lift {ℓ = b₂}) ∘ f≡g ∘ Level.lower {ℓ = a₂})

    -- Functional extensionality implies a form of extensionality for
    -- Π-types.

    ∀-extensionality : ∀ {a b} → Extensionality a (suc b) →
                       {A : Set a} (B₁ B₂ : A → Set b) →
                       (∀ x → B₁ x ≡ B₂ x) →
                       (∀ x → B₁ x) ≡ (∀ x → B₂ x)
    ∀-extensionality ext B₁ B₂ B₁≡B₂ with ext B₁≡B₂
    ... | refl = refl

    -- Extensionality for explicit function spaces implies extensionality
    -- for implicit function spaces.

    implicit-extensionality : ∀ {a b} →
                              Extensionality a b →
                              ExtensionalityImplicit a b
    implicit-extensionality ext f≡g = cong _$- (ext (λ x → f≡g))