------------------------------------------------------------------------
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4