Extensional equivalence of Lists and Vectors

VecList.agda

module VecList where

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

data List (A : Set) : Set where
  [] : List A
  _:>_ : A → List A → List A

data Vec (A : Set) : Nat → Set where
  [] : Vec A zero
  _:>_ : A → {n : Nat} → Vec A n → Vec A (suc n)

record RVec (A : Set) : Set where
  constructor rvec
  field
    {count} : Nat
    items : Vec A count

module ListRVec {A : Set} where
  there : List A → RVec A
  there [] = rvec []
  there (x :> xs) = rvec (x :> (RVec.items (there xs)))

  back : RVec A → List A
  back (rvec []) = []
  back (rvec (x :> items)) = x :> back (rvec items)

  left-id : (xs : List A) → back (there xs) ≡ xs
  left-id [] = refl
  left-id (x :> xs) rewrite left-id xs = refl

  right-id : (xs : RVec A) → there (back xs) ≡ xs
  right-id (rvec []) = refl
  right-id (rvec (x :> items)) rewrite right-id (rvec items) = refl

record _≅_ (A B : Set) : Set where
  constructor equiv
  field
    there : A → B
    back : B → A
    left-id : (a : A) → back (there a) ≡ a
    right-id : (b : B) → there (back b) ≡ b

LV : {A : Set} → List A ≅ RVec A
LV = record { ListRVec }

reflexivity : {A : Set} → A ≅ A
reflexivity = λ {A} → equiv (λ z → z) (λ z → z) (λ a → refl) (λ b → refl)

symmetry : {A B : Set} → A ≅ B → B ≅ A
symmetry (equiv there back left-id right-id) = equiv back there right-id left-id

transitivity : {A B C : Set} → A ≅ B → B ≅ C → A ≅ C
transitivity {A} {B} {C} (equiv thereAB backAB left-idAB right-idAB) (equiv thereBC backBC left-idBC right-idBC) =
  equiv thereAC backAC left-idAC right-idAC
  where
    thereAC : A → C
    thereAC c = thereBC (thereAB c)
    
    backAC : C → A
    backAC c = backAB (backBC c)

    left-idAC : (a : A) → backAC (thereAC a) ≡ a
    left-idAC a rewrite left-idBC (thereAB a) | left-idAB a = refl

    right-idAC : (c : C) → thereAC (backAC c) ≡ c
    right-idAC c rewrite right-idAB (backBC c) | right-idBC c = refl