refactor: deprecate injective⇒to⁻-cong

agda · Jan 29, 2025 · 576610f · 576610f
1 parent 8efb15d
commit 576610f
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda
@@ -93,4 +93,3 @@ injective⇒to⁻-cong = injective⇒section-cong
 "Warning: injective⇒to⁻-cong was deprecated in v2.3.
 Please use injective⇒section-cong instead. "
 #-}
-