Merge branch feature-get-record into feature-partial-getlen

These two features heavily interconnect. As such it makes sense to
integrate them properly. This non-trivial merge does that work. Compared
to feature-partial-getlen a few definitions moved from FreeTheorems.agda
to GetTypes.agda. Many types changed compared to both branches.

Conflicts:
	BFF.agda
	Bidir.agda
	FreeTheorems.agda
	Precond.agda
        conflict in GetTypes.agda not detected by merge

1 files changed, 16 insertions, 7 deletions

diff --git a/FreeTheorems.agda b/FreeTheorems.agda
index c22a68d..2181163 100644
--- a/FreeTheorems.agda
+++ b/FreeTheorems.agda
@@ -13,31 +13,40 @@ open Injection using (to)
 
 open import Generic using (≡-to-Π)
 
+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)
 
-  free-theorem-type : Set₁
-  free-theorem-type = {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get
+  open GetTypes.VecVec public
 
   postulate
-    free-theorem : free-theorem-type
+    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 }
 
 module PartialVecVec where
   get-type : {I : Setoid ℓ₀ ℓ₀} → (I ↪ (EqSetoid ℕ)) → (I ⟶ (EqSetoid ℕ)) → Set₁
   get-type {I} gl₁ gl₂ = {A : Set} {i : Setoid.Carrier I} → Vec A (to gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
 
+  open GetTypes.PartialVecVec public
+
   postulate
     free-theorem : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂)  → {α β : Set} → (f : α → β) → {i : Setoid.Carrier I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get
 
-  open VecVec using () renaming (free-theorem-type to VecVec-free-theorem-type)
-
-  VecVec-free-theorem : VecVec-free-theorem-type
-  VecVec-free-theorem {getlen} get = free-theorem Function.Injection.id (≡-to-Π getlen) get
+  assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂) → Get
+  assume-get {I} gl₁ gl₂ get = record { I = I; gl₁ = gl₁; gl₂ = gl₂; get = get; free-theorem = free-theorem gl₁ gl₂ get }