Skip to content

Data.Vec.Relation.Binary.Equality.Propositional.WithK

------------------------------------------------------------------------
-- The Agda standard library
--
-- Code related to vector equality over propositional equality that
-- makes use of heterogeneous equality
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Vec.Relation.Binary.Equality.Propositional.WithK
  {a} {A : Set a} where

open import Data.Vec.Base using (Vec)
open import Data.Vec.Relation.Binary.Equality.Propositional {A = A}
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Relation.Binary.HeterogeneousEquality using (_≅_; ≡-to-≅)

≋⇒≅ : ∀ {m n} {xs : Vec A m} {ys : Vec A n} →
      xs ≋ ys → xs ≅ ys
≋⇒≅ p with refl <- length-equal p = ≡-to-≅ (≋⇒≡ p)