Merge branch feature-get-record into master

This branch brings three main benefits:
 * Only one explicit parameter is needed to ask for a get function.
 * The postulated free theorems are mostly turned into preconditions,
   i.e. the only use of the postulates is in LiftGet.
 * We can now convert list based get functions to vec based ones and back
   including the (now) accompanying free theorem.

1 files changed, 20 insertions, 0 deletions

diff --git a/GetTypes.agda b/GetTypes.agda
new file mode 100644
index 0000000..99675f9
--- /dev/null
+++ b/GetTypes.agda
@@ -0,0 +1,20 @@
+module GetTypes where
+
+open import Data.Nat using (ℕ)
+open import Data.List using (List ; map)
+open import Data.Vec using (Vec) renaming (map to mapV)
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality using (_≗_)
+
+module ListList where
+  record Get : Set₁ where
+    field
+      get : {A : Set} → List A → List A
+      free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
+
+module VecVec where
+  record Get : Set₁ where
+    field
+      getlen : ℕ → ℕ
+      get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
+      free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get