Added some additional proofs about heterogenous equality and some res…

…ulting vector equality lemmas

CHANGELOG.md

@@ -575,6 +575,13 @@ Backwards compatible changes
   functor = record { _<$>_ = map}
   ```
 
+* Added proofs to `Data.Vec.Equality`
+  ```agda
+  to-≅      : xs ≈ ys → xs ≅ ys
+  xs++[]≈xs  : xs ++ [] ≈ xs
+  xs++[]≅xs : xs ++ [] ≅ xs
+  ```
+
 * Added proofs to `Data.Vec.Properties`
   ```agda
   lookup-map              : lookup i (map f xs) ≡ f (lookup i xs)
@@ -615,6 +622,12 @@ Backwards compatible changes
   P-resp⟶¬P-resp : Symmetric _≈_ → P Respects _≈_ → (¬_ ∘ P) Respects _≈_
   ```
 
+* Added conversion lemmas to `Relation.Binary.HeterogeneousEquality`
+  ```agda
+  ≅-to-type-≡  : {x : A} {y : B} → x ≅ y → A ≡ B
+  ≅-to-subst-≡ : (p : x ≅ y) → subst (λ x → x) (≅-to-type-≡ p) x ≡ y
+  ```
+
 Version 0.13
 ============
 

src/Data/Vec/Equality.agda

@@ -12,7 +12,7 @@ open import Function
 open import Level using (_⊔_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
-
+open import Relation.Binary.HeterogeneousEquality as H using (_≅_)
 module Equality {s₁ s₂} (S : Setoid s₁ s₂) where
 
   private
@@ -50,6 +50,10 @@ module Equality {s₁ s₂} (S : Setoid s₁ s₂) where
   trans (x≈y ∷-cong xs≈ys) (y≈z ∷-cong ys≈zs) =
     SS.trans x≈y y≈z ∷-cong trans xs≈ys ys≈zs
 
+  xs++[]≈xs : ∀ {n} (xs : Vec A n) → xs ++ [] ≈ xs
+  xs++[]≈xs []        = []-cong
+  xs++[]≈xs (x ∷ xs) = SS.refl ∷-cong (xs++[]≈xs xs)
+
   _++-cong_ : ∀ {n₁¹ n₂¹} {xs₁¹ : Vec A n₁¹} {xs₂¹ : Vec A n₂¹}
                 {n₁² n₂²} {xs₁² : Vec A n₁²} {xs₂² : Vec A n₂²} →
               xs₁¹ ≈ xs₁² → xs₂¹ ≈ xs₂² →
@@ -91,3 +95,11 @@ module PropositionalEquality {a} {A : Set a} where
 
   from-≡ : ∀ {n} {xs ys : Vec A n} → xs ≡ ys → xs ≈ ys
   from-≡ P.refl = refl _
+
+  to-≅ : ∀ {m n} {xs : Vec A m} {ys : Vec A n} →
+            xs ≈ ys → xs ≅ ys
+  to-≅ p with length-equal p
+  to-≅ p | P.refl = H.≡-to-≅ (to-≡ p)
+
+  xs++[]≅xs : ∀ {n} → (xs : Vec A n) → (xs ++ []) ≅ xs
+  xs++[]≅xs xs = to-≅ (xs++[]≈xs xs)

src/Relation/Binary/HeterogeneousEquality.agda

@@ -34,10 +34,18 @@ x ≇ y = ¬ x ≅ y
 ------------------------------------------------------------------------
 -- Conversion
 
+open Core public using (≅-to-≡)
+
 ≡-to-≅ : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≅ y
 ≡-to-≅ refl = refl
 
-open Core public using (≅-to-≡)
+≅-to-type-≡ : ∀ {a} {A B : Set a} {x : A} {y : B} →
+                x ≅ y → A ≡ B
+≅-to-type-≡ refl = refl
+
+≅-to-subst-≡ : ∀ {a} {A B : Set a} {x : A} {y : B} → (p : x ≅ y) →
+                 P.subst (λ x → x) (≅-to-type-≡ p) x ≡ y
+≅-to-subst-≡ refl = refl
 
 ------------------------------------------------------------------------
 -- Some properties