Added cong and map to vec ≋ equality (#1956)

Author: guilhermehas

CHANGELOG.md

@@ -3080,6 +3080,16 @@ This is a full list of proofs that have changed form to use irrelevant instance
   <-weakInduction-startingFrom : P i →  (∀ j → P (inject₁ j) → P (suc j)) → ∀ {j} → j ≥ i → P j
   ```
 
+* Added new function to `Data.Vec.Relation.Binary.Pointwise.Inductive`
+  ```agda
+  cong-[_]≔ : Pointwise _∼_ xs ys → Pointwise _∼_ (xs [ i ]≔ p) (ys [ i ]≔ p)
+  ```
+
+* Added new function to `Data.Vec.Relation.Binary.Equality.Setoid`
+  ```agda
+  map-[]≔ : map f (xs [ i ]≔ p) ≋ map f xs [ i ]≔ f p
+  ```
+
 * Added new function to `Data.List.Relation.Binary.Permutation.Propositional.Properties`
   ```agda
   ↭-reverse : (xs : List A) → reverse xs ↭ xs

src/Data/Vec/Relation/Binary/Equality/Setoid.agda

@@ -12,6 +12,7 @@ module Data.Vec.Relation.Binary.Equality.Setoid
   {a ℓ} (S : Setoid a ℓ) where
 
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Fin using (zero; suc)
 open import Data.Vec.Base
 open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
   using (Pointwise)
@@ -79,6 +80,12 @@ map-++ : ∀ {b m n} {B : Set b}
 map-++ f []       = ≋-refl
 map-++ f (x ∷ xs) = refl ∷ map-++ f xs
 
+map-[]≔ : ∀ {b n} {B : Set b}
+          (f : B → A) (xs : Vec B n) i p →
+          map f (xs [ i ]≔ p) ≋ map f xs [ i ]≔ f p
+map-[]≔ f (x ∷ xs) zero    p = refl ∷ ≋-refl
+map-[]≔ f (x ∷ xs) (suc i) p = refl ∷ map-[]≔ f xs i p
+
 ------------------------------------------------------------------------
 -- concat
 

src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda

@@ -217,6 +217,16 @@ module _ {_∼_ : REL A B ℓ} where
   tabulate⁻ (f₀∼g₀ ∷ _)   zero    = f₀∼g₀
   tabulate⁻ (_     ∷ f∼g) (suc i) = tabulate⁻ f∼g i
 
+------------------------------------------------------------------------
+-- cong
+
+module _ {_∼_ : Rel A ℓ} (refl : Reflexive _∼_) where
+  cong-[_]≔ : ∀ {n} i p {xs} {ys} →
+              Pointwise _∼_ {n} xs ys →
+              Pointwise _∼_ (xs [ i ]≔ p) (ys [ i ]≔ p)
+  cong-[ zero ]≔  p (_   ∷ eqn) = refl ∷ eqn
+  cong-[ suc i ]≔ p (x∼y ∷ eqn) = x∼y  ∷ cong-[ i ]≔ p eqn
+
 ------------------------------------------------------------------------
 -- Degenerate pointwise relations