drop the Function.Equality requirement from GetTypes

We never used the equality property. Thus a simple function is
sufficient here. We always fulfilled the property using ≡-to-Π anyway.

4 files changed, 37 insertions, 44 deletions

diff --git a/BFFPlug.agda b/BFFPlug.agda
index 5c219a5..a31d1bb 100644
--- a/BFFPlug.agda
+++ b/BFFPlug.agda
@@ -11,7 +11,6 @@ open import Relation.Binary using (module DecSetoid)
 open import Relation.Binary.PropositionalEquality using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq)
 open import Relation.Nullary using (yes ; no)
 open import Function using (flip ; id ; _∘_)
-open import Function.Equality using (_⟶_ ; _⟨$⟩_)
 open import Function.LeftInverse using (_RightInverseOf_)
 import Category.Monad
 open Category.Monad.RawMonad {ℓ₀} Data.Maybe.monad using (_>>=_)
@@ -37,20 +36,20 @@ bffplug G sput {i}     s v | just j | yes refl with bff G j s v
 ...                                            | nothing = nothing
 ...                                            | just s′ = just (j , s′)
 
-_SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set
+_SimpleRightInvOf_ : {A B : Set} → (A → B) → (B → A) → Set
 f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g
 
-bffinv : (G : Get) → (nelteg : PropEq ℕ ⟶ Get.I G) → nelteg RightInverseOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G (nelteg ⟨$⟩ m)))
-bffinv G nelteg inv {m = m} s v = bff G (nelteg ⟨$⟩ m) s (subst (Vec Carrier) (sym (inv m)) v)
+bffinv : (G : Get) → (nelteg : ℕ → Get.I G) → nelteg SimpleRightInvOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G (nelteg m)))
+bffinv G nelteg inv {m = m} s v = bff G (nelteg m) s (subst (Vec Carrier) (sym (inv m)) v)
 
 module InvExamples where
   open Examples using (reverse' ; drop' ; sieve' ; tail' ; take')
   
   reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m)
-  reverse-put s v = bffinv reverse' (≡-to-Π id) (λ _ → refl) s v >>= sequenceV
+  reverse-put s v = bffinv reverse' id (λ _ → refl) s v >>= sequenceV
 
   drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (k + m))
-  drop-put k = bffinv (drop' k) (≡-to-Π id) (λ _ → refl)
+  drop-put k = bffinv (drop' k) id (λ _ → refl)
 
   double : ℕ → ℕ
   double zero    = zero
@@ -62,10 +61,10 @@ module InvExamples where
   sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x)
 
   sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec (Maybe Carrier) (double m))
-  sieve-put = bffinv sieve' (≡-to-Π double) sieve-inv-len
+  sieve-put = bffinv sieve' double sieve-inv-len
 
   tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (suc m))
-  tail-put = bffinv tail' (≡-to-Π id) (λ _ → refl)
+  tail-put = bffinv tail' id (λ _ → refl)
 
   take-put : (k : ℕ) → {n : ℕ}  → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n))
   take-put k = bffsameshape (take' k)
diff --git a/Examples.agda b/Examples.agda
index ca65835..f30faa5 100644
--- a/Examples.agda
+++ b/Examples.agda
@@ -6,9 +6,8 @@ import Algebra.Structures
 open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop)
 open import Function using (id)
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong) renaming (setoid to EqSetoid)
+open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong)
 
-open import Generic using (≡-to-Π)
 open import Structures using (Shaped)
 import GetTypes
 import FreeTheorems
@@ -17,10 +16,10 @@ open GetTypes.PartialVecVec using (Get)
 open FreeTheorems.PartialVecVec using (assume-get)
 
 reverse' : Get
-reverse' = assume-get (≡-to-Π id) (≡-to-Π id) reverse
+reverse' = assume-get id id reverse
 
 double' : Get
-double' = assume-get (≡-to-Π id) (≡-to-Π g) f
+double' = assume-get id g f
   where g : ℕ → ℕ
         g zero = zero
         g (suc n) = suc (suc (g n))
@@ -29,19 +28,19 @@ double' = assume-get (≡-to-Π id) (≡-to-Π g) f
         f (x ∷ v) = x ∷ x ∷ f v
 
 double'' : Get
-double'' = assume-get (≡-to-Π id) (≡-to-Π _) (λ v → v ++ v)
+double'' = assume-get id _ (λ v → v ++ v)
 
 tail' : Get
-tail' = assume-get (≡-to-Π suc) (≡-to-Π id) tail
+tail' = assume-get suc id tail
 
 take' : ℕ → Get
-take' n = assume-get (≡-to-Π (_+_ n)) (≡-to-Π _) (take n)
+take' n = assume-get (_+_ n) _ (take n)
 
 drop' : ℕ → Get
-drop' n = assume-get (≡-to-Π (_+_ n)) (≡-to-Π _) (drop n)
+drop' n = assume-get (_+_ n) _ (drop n)
 
 sieve' : Get
-sieve' = assume-get (≡-to-Π id) (≡-to-Π _) f
+sieve' = assume-get id _ f
   where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉
         f []           = []
         f (x ∷ [])     = x ∷ []
@@ -58,7 +57,7 @@ intersperse s (x ∷ [])    = x ∷ []
 intersperse s (x ∷ y ∷ v) = x ∷ s ∷ intersperse s (y ∷ v)
 
 intersperse' : Get
-intersperse' = assume-get (≡-to-Π suc) (≡-to-Π intersperse-len) f
+intersperse' = assume-get suc intersperse-len f
   where f : {A : Set} {n : ℕ} → Vec A (suc n) → Vec A (intersperse-len n)
         f (s ∷ v)        = intersperse s v
 
diff --git a/FreeTheorems.agda b/FreeTheorems.agda
index 08bbe88..25759e0 100644
--- a/FreeTheorems.agda
+++ b/FreeTheorems.agda
@@ -5,9 +5,7 @@ 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 Function.Equality using (_⟶_ ; _⟨$⟩_)
-open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming (setoid to EqSetoid)
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality using (_≗_)
 
 import GetTypes
 
@@ -36,13 +34,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 (gl₁ ⟨$⟩ i) → Vec A (gl₂ ⟨$⟩ i)
+  get-type : {I : Set} → (I → ℕ) → (I → ℕ) → Set₁
+  get-type {I} gl₁ gl₂ = {A : Set} {i : 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 : Set} → (gl₁ : I → ℕ) → (gl₂ : I → ℕ) (get : get-type gl₁ gl₂)  → {α β : Set} → (f : α → β) → {i : 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 : Set} → (gl₁ : I → ℕ) → (gl₂ : I → ℕ) (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 }
diff --git a/GetTypes.agda b/GetTypes.agda
index 033257a..286b9aa 100644
--- a/GetTypes.agda
+++ b/GetTypes.agda
@@ -5,11 +5,8 @@ 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 (_∘_ ; id)
-open import Function.Equality using (_⟶_ ; _⟨$⟩_)
-open import Relation.Binary.PropositionalEquality using (_≗_) renaming (setoid to EqSetoid)
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality using (_≗_)
 
-open import Generic using (≡-to-Π)
 open import Structures using (Shaped ; module Shaped)
 open import Instances using (VecShaped)
 
@@ -29,13 +26,13 @@ module VecVec where
 module PartialVecVec where
   record Get : Set₁ where
     field
-      I : Setoid ℓ₀ ℓ₀
-      gl₁ : I ⟶ EqSetoid ℕ
-      gl₂ : I ⟶ EqSetoid ℕ
+      I : Set
+      gl₁ : I → ℕ
+      gl₂ : I → ℕ
 
-    |I|   = Setoid.Carrier I
-    |gl₁| = _⟨$⟩_ gl₁
-    |gl₂| = _⟨$⟩_ gl₂
+    |I|   = I
+    |gl₁| = gl₁
+    |gl₂| = gl₂
 
     field
       get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i)
@@ -43,9 +40,9 @@ module PartialVecVec where
 
 VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
 VecVec-to-PartialVecVec G = record
-  { I = EqSetoid ℕ
-  ; gl₁ = ≡-to-Π id
-  ; gl₂ = ≡-to-Π getlen
+  { I = ℕ
+  ; gl₁ = id
+  ; gl₂ = getlen
   ; get = get
   ; free-theorem = free-theorem
   } where open VecVec.Get G
@@ -61,13 +58,13 @@ module PartialShapeShape where
       ViewContainer : Set → ViewShape → Set
       ViewShapeT : Shaped ViewShape ViewContainer
 
-      I : Setoid ℓ₀ ℓ₀
-      gl₁ : I ⟶ EqSetoid SourceShape
-      gl₂ : I ⟶ EqSetoid ViewShape
+      I : Set
+      gl₁ : I → SourceShape
+      gl₂ : I → ViewShape
 
-    |I|   = Setoid.Carrier I
-    |gl₁| = _⟨$⟩_ gl₁
-    |gl₂| = _⟨$⟩_ gl₂
+    |I|   = I
+    |gl₁| = gl₁
+    |gl₂| = gl₂
 
     open Shaped SourceShapeT using () renaming (fmap to fmapS)
     open Shaped ViewShapeT using () renaming (fmap to fmapV)