From 9264ce29646025b3192b1eb2bea2e1683173d0cc Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Sat, 20 Oct 2018 16:30:29 +0100 Subject: [PATCH 1/3] Added Data.Vec.updateAt and its properties. --- CHANGELOG.md | 13 ++ src/Data/Vec.agda | 16 +- src/Data/Vec/Properties.agda | 171 ++++++++++++++---- .../Binary/PropositionalEquality.agda | 16 ++ 4 files changed, 180 insertions(+), 36 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 467d1eb21e..91ac28d508 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -659,6 +659,13 @@ Other minor additions align : Vec A m → Vec B n → Vec (These A B) (m ⊔ n) unzipWith : (A → B × C) → Vec A n → Vec B n × Vec C n ``` + A generalization of single point overwrite `_[_]≔_` + to single-point modification `_[_]%=_` + (alias with different argument order: `updateAt`): + ```agda + _[_]%=_ : Vec A n → Fin n → (A → A) → Vec A n + updateAt : Fin n → (A → A) → Vec A n → Vec A n + ``` * Added new proofs to `Data.Vec.All.Properties`: ```agda @@ -698,6 +705,8 @@ Other minor additions ```agda lookup-zipWith : lookup i (zipWith f xs ys) ≡ f (lookup i xs) (lookup i ys) ``` + Added laws for `updateAt`. + Now laws for `_[_]≔_` are special instances of these. * Added new proofs to `Data.Vec.Relation.Pointwise.Inductive`: ```agda @@ -885,6 +894,10 @@ Other minor additions <⇒≤ : _<_ ⇒ _≤_ ``` +* Added new definitions to `Relation.Binary.PropositionalEquality`: + - `_≡_↾¹_` equality of functions at a single point + - `_≡_↾_` equality of functions at a subset of the domain + * Added new proofs to `Relation.Binary.PropositionalEquality`: ```agda respˡ : ∼ Respectsˡ _≡_ diff --git a/src/Data/Vec.agda b/src/Data/Vec.agda index 10befc670a..16e4ea1812 100644 --- a/src/Data/Vec.agda +++ b/src/Data/Vec.agda @@ -58,11 +58,21 @@ remove (suc i) (x ∷ y ∷ xs) = x ∷ remove i (y ∷ xs) -- Update. -infixl 6 _[_]≔_ +infixl 6 _[_]%=_ _[_]≔_ + +-- updateAt i f xs modifies the i-th element of xs according to f + +updateAt : ∀ {a n} {A : Set a} → Fin n → (A → A) → Vec A n → Vec A n +updateAt zero f (x ∷ xs) = f x ∷ xs +updateAt (suc i) f (x ∷ xs) = x ∷ updateAt i f xs + +_[_]%=_ : ∀ {a n} {A : Set a} → Vec A n → Fin n → (A → A) → Vec A n +xs [ i ]%= f = updateAt i f xs + +-- xs [ i ]≔ y overwrites the i-th element of xs with y _[_]≔_ : ∀ {a n} {A : Set a} → Vec A n → Fin n → A → Vec A n -(x ∷ xs) [ zero ]≔ y = y ∷ xs -(x ∷ xs) [ suc i ]≔ y = x ∷ xs [ i ]≔ y +xs [ i ]≔ y = xs [ i ]%= λ _ → y ------------------------------------------------------------------------ -- Operations for transforming vectors diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index 27c1ff07b3..6f3f22cfcf 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -22,7 +22,7 @@ open import Function open import Function.Inverse using (_↔_; inverse) open import Relation.Binary hiding (Decidable) open import Relation.Binary.PropositionalEquality as P - using (_≡_; _≢_; refl; _≗_) + using (_≡_; _≢_; refl; _≗_; _≡_↾¹_) open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl) open import Relation.Unary using (Pred; Decidable) open import Relation.Nullary using (yes; no) @@ -70,66 +70,166 @@ module _ {a} {A : Set a} where lookup⇒[]= : ∀ {n} (i : Fin n) {x : A} xs → lookup i xs ≡ x → xs [ i ]= x lookup⇒[]= zero (_ ∷ _) refl = here - lookup⇒[]= (suc i) (_ ∷ xs) p = there (lookup⇒[]= i xs p) + lookup⇒[]= (suc i) (_ ∷ xs) p = there (lookup⇒[]= i xs p) []=↔lookup : ∀ {n i} {x} {xs : Vec A n} → xs [ i ]= x ↔ lookup i xs ≡ x []=↔lookup = inverse []=⇒lookup (lookup⇒[]= _ _) (λ _ → []=-irrelevance _ _) (λ _ → P.≡-irrelevance _ _) +------------------------------------------------------------------------ +-- updateAt (_[_]%=_) + +module _ {a} {A : Set a} where + + -- Defining properties of updateAt: + + -- (+) updateAt i actually updates the element at index i. + + updateAt-updates : ∀ {n} (i : Fin n) {f : A → A} (xs : Vec A n) {x : A} + → xs [ i ]= x + → updateAt i f xs [ i ]= f x + updateAt-updates zero (x ∷ xs) here = here + updateAt-updates (suc i) (x ∷ xs) (there loc) = there (updateAt-updates i xs loc) + + -- (-) updateAt i does not touch the elements at other indices. + + updateAt-minimal : ∀ {n} (i j : Fin n) {f : A → A} {x : A} (xs : Vec A n) + → i ≢ j + → xs [ i ]= x + → updateAt j f xs [ i ]= x + updateAt-minimal zero zero (x ∷ xs) 0≢0 here = ⊥-elim (0≢0 refl) + updateAt-minimal zero (suc j) (x ∷ xs) _ here = here + updateAt-minimal (suc i) zero (x ∷ xs) _ (there loc) = there loc + updateAt-minimal (suc i) (suc j) (x ∷ xs) i≢j (there loc) = + there (updateAt-minimal i j xs (i≢j ∘ P.cong suc) loc) + + -- The other properties are consequences of (+) and (-). + -- We spell the most natural properties out. + -- Direct inductive proofs are in most cases easier than just using + -- the defining properties. + + -- updateAt i is a morphism from the monoid of endofunctions A → A + -- to the monoid of endofunctions Vec A n → Vec A n + + -- 1a. relative identity: f = id ↾ (lookup i xs) + -- implies updateAt i f = id ↾ xs + + updateAt-id-relative : ∀ {n} (i : Fin n) (xs : Vec A n) {f : A → A} + → f ≡ id ↾¹ lookup i xs + → updateAt i f xs ≡ xs + updateAt-id-relative zero (x ∷ xs) eq = P.cong (_∷ xs) eq + updateAt-id-relative (suc i) (x ∷ xs) eq = P.cong (x ∷_) (updateAt-id-relative i xs eq) + + -- 1b. identity: updateAt i id ≗ id + + updateAt-id : ∀ {n} (i : Fin n) (xs : Vec A n) → + updateAt i id xs ≡ xs + updateAt-id i xs = updateAt-id-relative i xs refl + + -- 2. composition: updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g) + + updateAt-compose : ∀ {n} (i : Fin n) {f g : A → A} → + updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g) + updateAt-compose zero (x ∷ xs) = refl + updateAt-compose (suc i) (x ∷ xs) = P.cong (x ∷_) (updateAt-compose i xs) + + -- 3. congruence: updateAt i is a congruence wrt. extensional equality. + + -- 3a. If f = g ↾ (lookup i xs) + -- then updateAt i f = updateAt i g ↾ xs + + updateAt-cong-relative : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vec A n) + → f ≡ g ↾¹ lookup i xs + → updateAt i f xs ≡ updateAt i g xs + updateAt-cong-relative zero (x ∷ xs) f=g = P.cong (_∷ xs) f=g + updateAt-cong-relative (suc i) (x ∷ xs) f=g = P.cong (x ∷_) (updateAt-cong-relative i xs f=g) + + -- 3b. congruence: f ≗ g → updateAt i f ≗ updateAt i g + + updateAt-cong : ∀ {n} (i : Fin n) {f g : A → A} + → f ≗ g + → updateAt i f ≗ updateAt i g + updateAt-cong i f≗g xs = updateAt-cong-relative i xs (f≗g (lookup i xs)) + + -- The order of updates at different indices i ≢ j does not matter. + + -- This a consequence of updateAt-updates and updateAt-minimal + -- but easier to prove inductively. + + updateAt-commutes : ∀ {n} (i j : Fin n) {f g : A → A} + → i ≢ j + → updateAt i f ∘ updateAt j g ≗ updateAt j g ∘ updateAt i f + updateAt-commutes zero zero 0≢0 (x ∷ xs) = ⊥-elim (0≢0 refl) + updateAt-commutes zero (suc j) i≢j (x ∷ xs) = refl + updateAt-commutes (suc i) zero i≢j (x ∷ xs) = refl + updateAt-commutes (suc i) (suc j) i≢j (x ∷ xs) = + P.cong (x ∷_) (updateAt-commutes i j (i≢j ∘ P.cong suc) xs) + + -- lookup after updateAt reduces. + + -- For same index this is an easy consequence of updateAt-updates + -- using []=↔lookup. + + lookup∘updateAt : ∀ {n} (i : Fin n) {f : A → A} → + lookup i ∘ updateAt i f ≗ f ∘ lookup i + lookup∘updateAt i xs = + []=⇒lookup (updateAt-updates i xs (lookup⇒[]= i _ refl)) + + -- For different indices it easily follows from updateAt-minimal. + + lookup∘updateAt′ : ∀ {n} (i j : Fin n) {f : A → A} + → i ≢ j + → lookup i ∘ updateAt j f ≗ lookup i + lookup∘updateAt′ i j xs i≢j = + []=⇒lookup (updateAt-minimal i j i≢j xs (lookup⇒[]= i _ refl)) + + -- Aliases for notation _[_]%=_ + + []%=-id : ∀ {n} (xs : Vec A n) (i : Fin n) → xs [ i ]%= id ≡ xs + []%=-id xs i = updateAt-id i xs + + []%=-compose : ∀ {n} (xs : Vec A n) (i : Fin n) {f g : A → A} → + xs [ i ]%= f + [ i ]%= g + ≡ xs [ i ]%= g ∘ f + []%=-compose xs i = updateAt-compose i xs + ------------------------------------------------------------------------ -- _[_]≔_ (update) +-- +-- _[_]≔_ is defined in terms of updateAt, and all of its properties +-- are special cases of the ones for updateAt. module _ {a} {A : Set a} where []≔-idempotent : ∀ {n} (xs : Vec A n) (i : Fin n) {x₁ x₂ : A} → (xs [ i ]≔ x₁) [ i ]≔ x₂ ≡ xs [ i ]≔ x₂ - []≔-idempotent [] () - []≔-idempotent (x ∷ xs) zero = refl - []≔-idempotent (x ∷ xs) (suc i) = P.cong (x ∷_) ([]≔-idempotent xs i) + []≔-idempotent xs i = updateAt-compose i xs []≔-commutes : ∀ {n} (xs : Vec A n) (i j : Fin n) {x y : A} → i ≢ j → (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x - []≔-commutes [] () () _ - []≔-commutes (x ∷ xs) zero zero 0≢0 = ⊥-elim $ 0≢0 refl - []≔-commutes (x ∷ xs) zero (suc i) _ = refl - []≔-commutes (x ∷ xs) (suc i) zero _ = refl - []≔-commutes (x ∷ xs) (suc i) (suc j) i≢j = - P.cong (x ∷_) $ []≔-commutes xs i j (i≢j ∘ P.cong suc) + []≔-commutes xs i j i≢j = updateAt-commutes j i (i≢j ∘ P.sym) xs []≔-updates : ∀ {n} (xs : Vec A n) (i : Fin n) {x : A} → (xs [ i ]≔ x) [ i ]= x - []≔-updates [] () - []≔-updates (x ∷ xs) zero = here - []≔-updates (x ∷ xs) (suc i) = there ([]≔-updates xs i) + []≔-updates xs i = updateAt-updates i xs (lookup⇒[]= i xs refl) []≔-minimal : ∀ {n} (xs : Vec A n) (i j : Fin n) {x y : A} → i ≢ j → xs [ i ]= x → (xs [ j ]≔ y) [ i ]= x - []≔-minimal [] () () _ _ - []≔-minimal (x ∷ xs) .zero zero 0≢0 here = ⊥-elim (0≢0 refl) - []≔-minimal (x ∷ xs) .zero (suc j) _ here = here - []≔-minimal (x ∷ xs) (suc i) zero _ (there loc) = there loc - []≔-minimal (x ∷ xs) (suc i) (suc j) i≢j (there loc) = - there ([]≔-minimal xs i j (i≢j ∘ P.cong suc) loc) + []≔-minimal xs i j i≢j loc = updateAt-minimal i j xs i≢j loc []≔-lookup : ∀ {n} (xs : Vec A n) (i : Fin n) → xs [ i ]≔ lookup i xs ≡ xs - []≔-lookup [] () - []≔-lookup (x ∷ xs) zero = refl - []≔-lookup (x ∷ xs) (suc i) = P.cong (_∷_ x) $ []≔-lookup xs i + []≔-lookup xs i = updateAt-id-relative i xs refl lookup∘update : ∀ {n} (i : Fin n) (xs : Vec A n) x → lookup i (xs [ i ]≔ x) ≡ x - lookup∘update zero (_ ∷ xs) x = refl - lookup∘update (suc i) (_ ∷ xs) x = lookup∘update i xs x + lookup∘update i xs x = lookup∘updateAt i xs lookup∘update′ : ∀ {n} {i j : Fin n} → i ≢ j → ∀ (xs : Vec A n) y → lookup i (xs [ j ]≔ y) ≡ lookup i xs - lookup∘update′ {i = zero} {zero} i≢j xs y = ⊥-elim (i≢j refl) - lookup∘update′ {i = zero} {suc j} i≢j (x ∷ xs) y = refl - lookup∘update′ {i = suc i} {zero} i≢j (x ∷ xs) y = refl - lookup∘update′ {i = suc i} {suc j} i≢j (x ∷ xs) y = - lookup∘update′ (i≢j ∘ P.cong suc) xs y + lookup∘update′ {n} {i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs ------------------------------------------------------------------------ -- map @@ -155,12 +255,17 @@ lookup-map : ∀ {a b n} {A : Set a} {B : Set b} lookup-map zero f (x ∷ xs) = refl lookup-map (suc i) f (x ∷ xs) = lookup-map i f xs +map-updateAt : ∀ {n a b} {A : Set a} {B : Set b} → + ∀ {f : A → B} {g : A → A} {h : B → B} (xs : Vec A n) (i : Fin n) + → f ∘ g ≡ h ∘ f ↾¹ lookup i xs + → map f (updateAt i g xs) ≡ updateAt i h (map f xs) +map-updateAt (x ∷ xs) zero eq = P.cong (_∷ _) eq +map-updateAt (x ∷ xs) (suc i) eq = P.cong (_ ∷_) (map-updateAt xs i eq) + map-[]≔ : ∀ {n a b} {A : Set a} {B : Set b} (f : A → B) (xs : Vec A n) (i : Fin n) {x : A} → map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x -map-[]≔ f [] () -map-[]≔ f (x ∷ xs) zero = refl -map-[]≔ f (x ∷ xs) (suc i) = P.cong (_ ∷_) $ map-[]≔ f xs i +map-[]≔ f xs i = map-updateAt xs i refl ------------------------------------------------------------------------ -- _++_ diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index d062026425..c5faf4c1e7 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -99,6 +99,22 @@ _≗_ {A = A} {B} = Setoid._≈_ (A →-setoid B) (A → Setoid.Carrier B) → setoid A ⟶ B →-to-⟶ = :→-to-Π +-- Equality of functions at a single point + +infix 4 _≡_↾¹_ + +_≡_↾¹_ : ∀{a b} {A : Set a} {B : Set b} (f g : A → B) (x : A) → Set b +f ≡ g ↾¹ x = f x ≡ g x + +-- Equality of functions on a subset of the domain + +infix 4 _≡_↾_ + +_≡_↾_ : ∀{a b p} {A : Set a} {B : Set b} + (f g : A → B) (P : A → Set p) → Set (a ⊔ b ⊔ p) +f ≡ g ↾ P = ∀{x} → P x → f x ≡ g x + + ------------------------------------------------------------------------ -- Inspect From 520ce90c915925140021af139c4d680f2c1a2b1b Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 25 Dec 2018 20:11:30 +0100 Subject: [PATCH 2/3] [ #510 ] Added Data.Vec.Properties.updateAt-compose-relative Suggested by Guillaume Allais for consistency. Note that it is equal to updateAt-cong-relative after updateAt-compose. --- src/Data/Vec/Properties.agda | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index c3bcbce808..e989434e0f 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -140,12 +140,21 @@ module _ {a} {A : Set a} where updateAt i id xs ≡ xs updateAt-id i xs = updateAt-id-relative i xs refl - -- 2. composition: updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g) + -- 2a. relative composition: f ∘ g = h ↾ (lookup i xs) + -- implies updateAt i f ∘ updateAt i g ≗ updateAt i h + + updateAt-compose-relative : ∀ {n} (i : Fin n) {f g h : A → A} (xs : Vec A n) + → f ∘ g ≡ h ↾¹ lookup i xs + → updateAt i f (updateAt i g xs) ≡ updateAt i h xs + updateAt-compose-relative zero (x ∷ xs) fg=h = P.cong (_∷ xs) fg=h + updateAt-compose-relative (suc i) (x ∷ xs) fg=h = + P.cong (x ∷_) (updateAt-compose-relative i xs fg=h) + + -- 2b. composition: updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g) updateAt-compose : ∀ {n} (i : Fin n) {f g : A → A} → updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g) - updateAt-compose zero (x ∷ xs) = refl - updateAt-compose (suc i) (x ∷ xs) = P.cong (x ∷_) (updateAt-compose i xs) + updateAt-compose i xs = updateAt-compose-relative i xs refl -- 3. congruence: updateAt i is a congruence wrt. extensional equality. @@ -727,3 +736,6 @@ module _ {a} {A : Set a} where toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs toList∘fromList List.[] = refl toList∘fromList (x List.∷ xs) = P.cong (x List.∷_) (toList∘fromList xs) + +-- -} +-- -} From 0156aee28e335554979b4566d577e791685c43c9 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Tue, 25 Dec 2018 20:22:35 +0100 Subject: [PATCH 3/3] =?UTF-8?q?[=20#510=20]=20Removed=20=5F=E2=89=A1=5F?= =?UTF-8?q?=E2=86=BE=C2=B9=5F=20notation=20for=20equality=20of=20functions?= =?UTF-8?q?=20at=20one=20point.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Vec/Properties.agda | 17 ++++++++++------- src/Relation/Binary/PropositionalEquality.agda | 16 ---------------- 2 files changed, 10 insertions(+), 23 deletions(-) diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda index e989434e0f..dd38031f11 100644 --- a/src/Data/Vec/Properties.agda +++ b/src/Data/Vec/Properties.agda @@ -24,7 +24,7 @@ open import Function open import Function.Inverse using (_↔_; inverse) open import Relation.Binary hiding (Decidable) open import Relation.Binary.PropositionalEquality as P - using (_≡_; _≢_; refl; _≗_; _≡_↾¹_) + using (_≡_; _≢_; refl; _≗_) open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl) open import Relation.Unary using (Pred; Decidable) open import Relation.Nullary using (yes; no) @@ -122,14 +122,17 @@ module _ {a} {A : Set a} where -- Direct inductive proofs are in most cases easier than just using -- the defining properties. - -- updateAt i is a morphism from the monoid of endofunctions A → A - -- to the monoid of endofunctions Vec A n → Vec A n + -- In the explanations, we make use of shorthand f = g ↾ x + -- meaning that f and g agree at point x, i.e. f x ≡ g x. + + -- updateAt i is a morphism from the monoid of endofunctions A → A + -- to the monoid of endofunctions Vec A n → Vec A n -- 1a. relative identity: f = id ↾ (lookup i xs) -- implies updateAt i f = id ↾ xs updateAt-id-relative : ∀ {n} (i : Fin n) (xs : Vec A n) {f : A → A} - → f ≡ id ↾¹ lookup i xs + → f (lookup i xs) ≡ lookup i xs → updateAt i f xs ≡ xs updateAt-id-relative zero (x ∷ xs) eq = P.cong (_∷ xs) eq updateAt-id-relative (suc i) (x ∷ xs) eq = P.cong (x ∷_) (updateAt-id-relative i xs eq) @@ -144,7 +147,7 @@ module _ {a} {A : Set a} where -- implies updateAt i f ∘ updateAt i g ≗ updateAt i h updateAt-compose-relative : ∀ {n} (i : Fin n) {f g h : A → A} (xs : Vec A n) - → f ∘ g ≡ h ↾¹ lookup i xs + → f (g (lookup i xs)) ≡ h (lookup i xs) → updateAt i f (updateAt i g xs) ≡ updateAt i h xs updateAt-compose-relative zero (x ∷ xs) fg=h = P.cong (_∷ xs) fg=h updateAt-compose-relative (suc i) (x ∷ xs) fg=h = @@ -162,7 +165,7 @@ module _ {a} {A : Set a} where -- then updateAt i f = updateAt i g ↾ xs updateAt-cong-relative : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vec A n) - → f ≡ g ↾¹ lookup i xs + → f (lookup i xs) ≡ g (lookup i xs) → updateAt i f xs ≡ updateAt i g xs updateAt-cong-relative zero (x ∷ xs) f=g = P.cong (_∷ xs) f=g updateAt-cong-relative (suc i) (x ∷ xs) f=g = P.cong (x ∷_) (updateAt-cong-relative i xs f=g) @@ -279,7 +282,7 @@ lookup-map (suc i) f (x ∷ xs) = lookup-map i f xs map-updateAt : ∀ {n a b} {A : Set a} {B : Set b} → ∀ {f : A → B} {g : A → A} {h : B → B} (xs : Vec A n) (i : Fin n) - → f ∘ g ≡ h ∘ f ↾¹ lookup i xs + → f (g (lookup i xs)) ≡ h (f (lookup i xs)) → map f (updateAt i g xs) ≡ updateAt i h (map f xs) map-updateAt (x ∷ xs) zero eq = P.cong (_∷ _) eq map-updateAt (x ∷ xs) (suc i) eq = P.cong (_ ∷_) (map-updateAt xs i eq) diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index b51983d9b5..21f7244ee0 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -112,22 +112,6 @@ _≗_ {A = A} {B} = Setoid._≈_ (A →-setoid B) (A → Setoid.Carrier B) → setoid A ⟶ B →-to-⟶ = :→-to-Π --- Equality of functions at a single point - -infix 4 _≡_↾¹_ - -_≡_↾¹_ : ∀{a b} {A : Set a} {B : Set b} (f g : A → B) (x : A) → Set b -f ≡ g ↾¹ x = f x ≡ g x - --- Equality of functions on a subset of the domain - -infix 4 _≡_↾_ - -_≡_↾_ : ∀{a b p} {A : Set a} {B : Set b} - (f g : A → B) (P : A → Set p) → Set (a ⊔ b ⊔ p) -f ≡ g ↾ P = ∀{x} → P x → f x ≡ g x - - ------------------------------------------------------------------------ -- Inspect