replace rewrite with cong where feasible
[~helmut/bidiragda.git] / GetTypes.agda
1 module GetTypes where
2
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 (_≗_)
8
9 module ListList where
10   record Get : Set₁ where
11     field
12       get : {A : Set} → List A → List A
13       free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
14
15 module VecVec where
16   record Get : Set₁ where
17     field
18       getlen : ℕ → ℕ
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