1
1
------------------------------------------------------------------------
2
-- The Agda standard library
2
4
-- Propositional (intensional) equality
3
5
------------------------------------------------------------------------
5
{-# OPTIONS --universe-polymorphism #-}
7
7
module Relation.Binary.PropositionalEquality where
10
10
open import Function.Equality using (Π; _⟶_; ≡-setoid)
11
11
open import Data.Product
12
open import Data.Unit.Core
13
14
open import Relation.Binary
14
15
import Relation.Binary.Indexed as I
15
16
open import Relation.Binary.Consequences
17
open import Relation.Binary.HeterogeneousEquality.Core as H using (_≅_)
17
19
-- Some of the definitions can be found in the following modules:
95
97
------------------------------------------------------------------------
98
data Inspect {a} {A : Set a} (x : A) : Set a where
99
_with-≡_ : (y : A) (eq : x ≡ y) → Inspect x
101
inspect : ∀ {a} {A : Set a} (x : A) → Inspect x
102
inspect x = x with-≡ refl
98
-- The old inspect idiom
100
-- The old inspect idiom has been deprecated, and may be removed in
101
-- the future. Use inspect on steroids instead.
103
module Deprecated-inspect where
105
-- The inspect idiom can be used when you want to pattern match on
106
-- the result r of some expression e, and you also need to
107
-- "remember" that r ≡ e.
109
-- The inspect idiom has a problem: sometimes you can only pattern
110
-- match on the p part of p with-≡ eq if you also pattern match on
111
-- the eq part, and then you no longer have access to the equality.
112
-- Inspect on steroids solves this problem.
114
data Inspect {a} {A : Set a} (x : A) : Set a where
115
_with-≡_ : (y : A) (eq : x ≡ y) → Inspect x
117
inspect : ∀ {a} {A : Set a} (x : A) → Inspect x
118
inspect x = x with-≡ refl
122
-- f x y with inspect (g x)
123
-- f x y | c z with-≡ eq = ...
125
------------------------------------------------------------------------
126
-- Inspect on steroids
128
-- Inspect on steroids can be used when you want to pattern match on
129
-- the result r of some expression e, and you also need to "remember"
132
data Reveal_is_ {a} {A : Set a} (x : Hidden A) (y : A) : Set a where
133
[_] : (eq : reveal x ≡ y) → Reveal x is y
135
inspect : ∀ {a b} {A : Set a} {B : A → Set b}
136
(f : (x : A) → B x) (x : A) → Reveal (hide f x) is (f x)
137
inspect f x = [ refl ]
104
139
-- Example usage:
141
-- f x y with g x | inspect g x
142
-- f x y | c z | [ eq ] = ...
107
144
------------------------------------------------------------------------
108
145
-- Convenient syntax for equational reasoning
127
158
hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _≡⟨_⟩_)
128
159
open Dummy public
163
_≅⟨_⟩_ : ∀ {a} {A : Set a} (x : A) {y z : A} →
164
x ≅ y → y IsRelatedTo z → x IsRelatedTo z
165
_ ≅⟨ x≅y ⟩ y≡z = _ ≡⟨ H.≅-to-≡ x≅y ⟩ y≡z
130
167
------------------------------------------------------------------------
168
-- Functional extensionality
132
170
-- If _≡_ were extensional, then the following statement could be
137
174
Extensionality a b =
138
175
{A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
139
176
(∀ x → f x ≡ g x) → f ≡ g
178
-- If extensionality holds for a given universe level, then it also
179
-- holds for lower ones.
181
extensionality-for-lower-levels :
183
Extensionality (a₁ ⊔ a₂) (b₁ ⊔ b₂) → Extensionality a₁ b₁
184
extensionality-for-lower-levels a₂ b₂ ext f≡g =
185
cong (λ h → lower ∘ h ∘ lift) $
186
ext (cong (lift {ℓ = b₂}) ∘ f≡g ∘ lower {ℓ = a₂})
188
-- Functional extensionality implies a form of extensionality for
193
Extensionality a (suc b) →
194
{A : Set a} (B₁ B₂ : A → Set b) →
195
(∀ x → B₁ x ≡ B₂ x) → (∀ x → B₁ x) ≡ (∀ x → B₂ x)
196
∀-extensionality ext B₁ B₂ B₁≡B₂ with ext B₁≡B₂
197
∀-extensionality ext B .B B₁≡B₂ | refl = refl
added
removed
src/Relation/Binary/PropositionalEquality.agda
