Function equality based on parameterizing over Relation.Binary.PropositionalEquality.Extensionality

ExtensionalEquilaity.agda

module ExtensionalEquality where
  open import Level
  open import Relation.Binary
  open import Relation.Binary.PropositionalEquality
  open import Function using (_$_; id)

  infix 4 _≈_

  data _≈_ {ℓ} {A : Set ℓ} : Rel A (suc ℓ) where
    ≈-inj : ∀ {x y} → (x~y : ∀ (ext : Extensionality ℓ ℓ) → x ≡ y) → x ≈ y

-- _≈_ is an equivalence relation

  ≈-refl : ∀ {ℓ} {A : Set ℓ} → Reflexive (_≈_ {A = A})
  ≈-refl = ≈-inj (λ _ → refl)

  ≈-sym : ∀ {ℓ} {A : Set ℓ} → Symmetric (_≈_ {A = A})
  ≈-sym (≈-inj i~j) = ≈-inj $
    λ ext → sym (i~j ext)

  ≈-trans : ∀ {ℓ} {A : Set ℓ} → Transitive (_≈_ {A = A})
  ≈-trans (≈-inj i~j) (≈-inj j~k) = ≈-inj $
    λ ext → trans (i~j ext) (j~k ext)

  ≈-isEquivalence : ∀ {ℓ} {A : Set ℓ} → IsEquivalence (_≈_ {A = A})
  ≈-isEquivalence = record {
      refl  = ≈-refl ;
      sym   = ≈-sym ;
      trans = ≈-trans
    }

-- Some properties

  ≈-cong : ∀ {a} {A B : Set a} (f : A → B) {x y}
         → x ≈ y → f x ≈ f y
  ≈-cong {a} {b} f (≈-inj x~y) = ≈-inj $
    λ ext → cong f (x~y (extensionality-for-lower-levels a a ext))

  ≈-cong-app : ∀ {a b} {A : Set a} {B : A → Set (a ⊔ b)} {f g : (x : A) → B x}
             → f ≈ g → (x : A) → f x ≈ g x
  ≈-cong-app (≈-inj f~g) x = ≈-inj $
    λ ext → cong-app (f~g ext) x

  ≈-cong₂ : ∀ {a b} {A : Set a} {B : Set b} {C : Set (a ⊔ b)} (f : A → B → C) {x y u v}
          → x ≈ y → u ≈ v → f x u ≈ f y v
  ≈-cong₂ {a} {b} {c} f (≈-inj x~y) (≈-inj u~v) = ≈-inj $
    λ ext → cong₂ f (x~y (extensionality-for-lower-levels (a ⊔ b) (a ⊔ b) ext))
                    (u~v (extensionality-for-lower-levels (a ⊔ b) (a ⊔ b) ext))

  ≈-setoid : ∀ {ℓ} (A : Set ℓ) → Setoid _ _
  ≈-setoid A = record {
      Carrier       = A ;
      _≈_           = _≈_ ;
      isEquivalence = ≈-isEquivalence
    }

  ≈-decSetoid : ∀ {ℓ} {A : Set ℓ} → Decidable (_≈_ {A = A}) → DecSetoid _ _
  ≈-decSetoid dec = record {
      _≈_              = _≈_ ;
      isDecEquivalence = record {
        isEquivalence = ≈-isEquivalence ;
        _≟_           = dec
      }
    }

  ≈-isPreorder : ∀ {ℓ} {A : Set ℓ} → IsPreorder {A = A} _≈_ _≈_
  ≈-isPreorder = record {
      isEquivalence = ≈-isEquivalence ;
      reflexive     = id ;
      trans         = ≈-trans
    }

  ≈-preorder : ∀ {a} → Set a → Preorder _ _ _
  ≈-preorder A = record {
      Carrier    = A ;
      _≈_        = _≈_ ;
      _∼_        = _≈_ ;
      isPreorder = ≈-isPreorder
    }