[ new ] updateAt and extra Properties on List.All

CHANGELOG.md

@@ -952,10 +952,6 @@ Other minor additions
   ×-magma : Symmetric-kind → (ℓ : Level) → Magma _ _
   ```
 
-* 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.Consequences`:
   ```agda
   wlog : Total _R_ → Symmetric Q → (∀ a b → a R b → Q a b) → ∀ a b → Q a b

src/Data/Vec/Properties.agda

@@ -129,14 +129,11 @@ module _ {a} {A : Set a} where
   -- Direct inductive proofs are in most cases easier than just using
   -- the defining properties.
 
-  -- 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
 
-  -- 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
+  -- 1a. relative identity:  f (lookup i xs) = lookup i xs
+  --                implies  updateAt i f xs = xs
 
   updateAt-id-relative : ∀ {n} (i : Fin n) (xs : Vec A n) {f : A → A}
     → f (lookup i xs) ≡ lookup i xs
@@ -150,7 +147,7 @@ module _ {a} {A : Set a} where
     updateAt i id xs ≡ xs
   updateAt-id i xs = updateAt-id-relative i xs refl
 
-  -- 2a. relative composition:  f ∘ g = h ↾ (lookup i xs)
+  -- 2a. relative composition:  (f ∘ g) (lookup i xs) = 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)
@@ -164,12 +161,13 @@ module _ {a} {A : Set a} where
 
   updateAt-compose : ∀ {n} (i : Fin n) {f g : A → A} →
     updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g)
-  updateAt-compose i xs = updateAt-compose-relative i xs refl
+  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
+  -- 3a.  If    f (lookup i xs) = g (lookup i xs)
+  --      then  updateAt i f xs = updateAt i g xs
 
   updateAt-cong-relative : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vec A n)
     → f (lookup i xs) ≡ g (lookup i xs)