diff --git a/src/1Lab/Extensionality.agda b/src/1Lab/Extensionality.agda
index 508cd89df..7af01f6b1 100644
--- a/src/1Lab/Extensionality.agda
+++ b/src/1Lab/Extensionality.agda
@@ -290,6 +290,16 @@ iso→extensional
 iso→extensional f ext =
   embedding→extensional (Iso→Embedding f) ext
 
+injection→extensional
+  : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
+  → is-set B
+  → {f : A → B}
+  → (∀ {x y} → f x ≡ f y → x ≡ y)
+  → Extensional B ℓr
+  → Extensional A ℓr
+injection→extensional b-set {f} inj ext =
+  embedding→extensional (f , injective→is-embedding b-set f inj) ext
+
 injection→extensional!
   : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : Type ℓ'}
   → {@(tactic hlevel-tactic-worker) sb : is-set B}
@@ -297,5 +307,4 @@ injection→extensional!
   → (∀ {x y} → f x ≡ f y → x ≡ y)
   → Extensional B ℓr
   → Extensional A ℓr
-injection→extensional! {sb = b-set} {f} inj ext =
-  embedding→extensional (f , injective→is-embedding b-set f inj) ext
+injection→extensional! {sb = b-set} = injection→extensional b-set