open import 1Lab.Path open import 1Lab.Type open import Data.Product.NAry open import Data.Fin.Base open import Data.Nat.Base module Data.Vec.Base where
Vectorsπ
The type Vec is a representation of n-ary tuples with coordinates drawn from A. Therefore, it is equivalent to the type , i.e., the functions from the with elements to the type . The halves of this equivalence are called lookup and tabulate.
data Vec {β} (A : Type β) : Nat β Type β where [] : Vec A zero _β·_ : β {n} β A β Vec A n β Vec A (suc n) Vec-elim : β {β ββ²} {A : Type β} (P : β {n} β Vec A n β Type ββ²) β P [] β (β {n} x (xs : Vec A n) β P xs β P (x β· xs)) β β {n} (xs : Vec A n) β P xs Vec-elim P p[] pβ· [] = p[] Vec-elim P p[] pβ· (x β· xs) = pβ· x xs (Vec-elim P p[] pβ· xs) infixr 20 _β·_ private variable β : Level A B : Type β n k : Nat lookup : Vec A n β Fin n β A lookup (x β· xs) fzero = x lookup (x β· xs) (fsuc i) = lookup xs i
tabulate : (Fin n β A) β Vec A n tabulate {zero} f = [] tabulate {suc n} f = f fzero β· tabulate (Ξ» x β f (fsuc x)) map : (A β B) β Vec A n β Vec B n map f [] = [] map f (x β· xs) = f x β· map f xs instance From-prod-Vec : From-product A (Vec A) From-prod-Vec .From-product.from-prod = go where go : β n β Vecβ A n β Vec A n go zero xs = [] go (suc zero) xs = xs β· [] go (suc (suc n)) (x , xs) = x β· go (suc n) xs _ : Path (Vec Nat 3) [ 1 , 2 , 3 ] (1 β· 2 β· 3 β· []) _ = refl