index c22a68d..2181163 100644 (file)
@@ -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 }