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

{-# OPTIONS --without-K --safe #-}

module Axiom.Extensionality.Propositional where

open import Function
open import Level using (Level; _⊔_; suc; lift)
open import Relation.Binary.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 : 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))