chore: add a non-tactic version of injection→extensional! (#308)

the1lab · Dec 11, 2023 · 2272186 · 2272186
1 parent 6477dac
commit 2272186
Showing 1 changed file with 11 additions and 2 deletions.
diff --git a/src/1Lab/Extensionality.agda b/src/1Lab/Extensionality.agda
@@ -290,12 +290,21 @@ 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}
   → {f : A → B}
   → (∀ {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