3 open import Data.Nat using (ℕ)
4 open import Data.List using (List ; map)
5 open import Data.Vec using (Vec) renaming (map to mapV)
6 open import Function using (_∘_)
7 open import Relation.Binary.PropositionalEquality using (_≗_)
10 record Get : Set₁ where
12 get : {A : Set} → List A → List A
13 free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
16 record Get : Set₁ where
19 get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
20 free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get