VecIIR.agda

open import Data.Nat
open import Data.Fin renaming ( zero to here ; suc to there )
open import Data.Product
open import Relation.Binary.PropositionalEquality
module _ where

mutual
 data Vec₁ (A : Set) : ℕ → Set where
   nil₁ : Vec₁ A zero
   cons₁ : {n : ℕ} → A → (xs : Vec₁ A n) → toℕ (Vec₂ xs) ≡ n → Vec₁ A (suc n)

 Vec₂ : {A : Set}{n : ℕ} → Vec₁ A n → Fin (suc n)
 Vec₂ nil₁ = here
 Vec₂ (cons₁ x xs q) = there (Vec₂ xs)

Vec : Set → ℕ → Set
Vec A n = Σ (Vec₁ A n) (λ xs → toℕ (Vec₂ xs) ≡ n)

nil : {A : Set} → Vec A zero
nil = nil₁ , refl

cons : {A : Set} {n : ℕ} → A → Vec A n → Vec A (suc n)
cons x (xs , q) = cons₁ x xs q , cong suc q