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.

1 files changed, 7 insertions, 8 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)