chore: add a non-tactic version of injection→extensional!

[favonia]

Description

I encountered a case where set-ness has to be passed as an (instance or implicit) argument to Extensional because I could not find a clean and usable way to bundle setness with other types. The best solution I found is to use an implicit argument with a tactic to get the set-ness "intelligently", and then pass the set-ness proof to injection→extensional. (The tactic in injection→extensional!, unfortunately, did not work because it would see (x y : A) -> is-prop (Path A x y) instead of is-set A at that point.) While I could specify the implicit argument of injection→extensional! using {sb = ...}, I felt this is a bit fragile and maybe it's cleaner to have a non-tactical version of injection→extensional. Thus this PR.

Checklist

Before submitting a merge request, please check the items below:

• I've read the contributing guidelines.
• The imports of new modules have been sorted with support/sort-imports.hs.
• All new code blocks have "agda" as their language.