1 files changed, 0 insertions, 3 deletions
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)