remove unused imports

Most of the became unused by using the convenience functions introduced
in the parent commit.

4 files changed, 1 insertions, 13 deletions

diff --git a/BFF.agda b/BFF.agda
index f5573ba..ced6ebf 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -11,11 +11,7 @@ open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
 open import Data.List using (List ; [] ; _∷_ ; map ; length)
 open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_)
 open import Function using (id ; _∘_ ; flip)
-open import Function.Equality using (_⟶_ ; _⟨$⟩_)
-open import Function.Injection using (module Injection) renaming (Injection to _↪_ ; id to id↪)
 open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid)
-open import Relation.Binary.PropositionalEquality using (cong) renaming (setoid to EqSetoid)
-open Injection using (to)
 
 open import FinMap
 open import Generic using (mapMV ; ≡-to-Π)
diff --git a/Bidir.agda b/Bidir.agda
index a77a9db..cca2ba7 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -18,9 +18,6 @@ open import Data.Vec.Equality using () renaming (module Equality to VecEq)
 open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate ; map-cong ; map-∘)
 open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
 open import Function using (id ; _∘_ ; flip)
-open import Function.Equality using (_⟶_ ; _⟨$⟩_)
-open import Function.Injection using (module Injection) renaming (Injection to _↪_)
-open Injection using (to)
 open import Relation.Binary.Core using (refl ; _≡_)
 open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
 open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans ; cong₂ ; decSetoid ; module ≡-Reasoning) renaming (setoid to EqSetoid)
diff --git a/FreeTheorems.agda b/FreeTheorems.agda
index 2181163..d4eb174 100644
--- a/FreeTheorems.agda
+++ b/FreeTheorems.agda
@@ -11,8 +11,6 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming
 open import Relation.Binary using (Setoid)
 open Injection using (to)
 
-open import Generic using (≡-to-Π)
-
 import GetTypes
 
 module ListList where
diff --git a/Precond.agda b/Precond.agda
index 81c204b..ebb5412 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -20,11 +20,8 @@ open Data.List.Any.Membership-≡ using (_∉_)
 open import Data.Maybe using (just)
 open import Data.Product using (∃ ; _,_ ; proj₂)
 open import Function using (flip ; _∘_ ; id)
-open import Function.Equality using (_⟶_ ; _⟨$⟩_)
-open import Function.Injection using (module Injection) renaming (Injection to _↪_)
-open Injection using (to)
 open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) renaming (setoid to EqSetoid)
+open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Relation.Nullary using (yes ; no)