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, 12 insertions, 0 deletions

diff --git a/FreeTheorems.agda b/FreeTheorems.agda
index f37cada..2695491 100644
--- a/FreeTheorems.agda
+++ b/FreeTheorems.agda
@@ -6,16 +6,28 @@ open import Data.Vec using (Vec) renaming (map to mapV)
 open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality using (_≗_)
 
+import GetTypes
+
 module ListList where
   get-type : Set₁
   get-type = {A : Set} → List A → List A
 
+  open GetTypes.ListList public
+
   postulate
     free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
 
+  assume-get : get-type → Get
+  assume-get get = record { get = get; free-theorem = free-theorem get }
+
 module VecVec where
   get-type : (ℕ → ℕ) → Set₁
   get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
 
+  open GetTypes.VecVec public
+
   postulate
     free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
+
+  assume-get : {getlen : ℕ → ℕ} → (get : get-type getlen) → Get
+  assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get }