drop the injection requirement for gl₁

Turns out, we never use this requirement. The only place where it may
come in relevant is the free theorems. But here non-injectivity turns
out to be reasoning about multiple get functions that are selected by
the additional index each individually satisfying the free theorem and
thus commonly satisfying it as well.

1 files changed, 4 insertions, 6 deletions

diff --git a/FreeTheorems.agda b/FreeTheorems.agda
index d4eb174..08bbe88 100644
--- a/FreeTheorems.agda
+++ b/FreeTheorems.agda
@@ -6,10 +6,8 @@ open import Data.List using (List ; map)
 open import Data.Vec using (Vec) renaming (map to mapV)
 open import Function using (_∘_)
 open import Function.Equality using (_⟶_ ; _⟨$⟩_)
-open import Function.Injection using (module Injection) renaming (Injection to _↪_)
 open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming (setoid to EqSetoid)
 open import Relation.Binary using (Setoid)
-open Injection using (to)
 
 import GetTypes
 
@@ -38,13 +36,13 @@ module VecVec where
   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)
+  get-type : {I : Setoid ℓ₀ ℓ₀} → (I ⟶ EqSetoid ℕ) → (I ⟶ EqSetoid ℕ) → Set₁
+  get-type {I} gl₁ gl₂ = {A : Set} {i : Setoid.Carrier I} → Vec A (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
+    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
 
-  assume-get : {I : Setoid ℓ₀ ℓ₀} → (gl₁ : I ↪ (EqSetoid ℕ)) → (gl₂ : I ⟶ (EqSetoid ℕ)) (get : get-type gl₁ gl₂) → 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 }