chore(CategoryTheory/EpiMono): use to_dual

[JovanGerb]

Generate declarations about Mono, SplitMono and SplitMonoCategory from the epic versions.

---

[github-actions]

PR summary 82df34056b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

++ because
- IsIso.of_mono_retraction
- IsIso.of_mono_retraction'
- IsSplitMono.id
- IsSplitMono.mk'
- SplitMono.comp
- SplitMono.map
- SplitMono.mono
- SplitMono.op
- SplitMono.splitEpi
- instance (priority := 100) IsSplitMono.mono {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] : Mono f
- instance (priority := 100) IsSplitMono.of_iso {X Y : C} (f : X ⟶ Y) [IsIso f] : IsSplitMono f
- instance [IsSplitEpi f] : IsSplitMono f.op
- instance {X Y : C} (f : X ⟶ Y) [hf : IsSplitMono f] (F : C ⥤ D) : IsSplitMono (F.map f)
- instance {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [hf : IsSplitMono f] [hg : IsSplitMono g] :
- isIso_of_epi_of_isSplitMono
- isSplitMono_of_mono
- mono_comp_iff_of_isIso
- mono_comp_iff_of_mono
- op_mono_iff
- op_mono_of_epi
- retraction
- retraction_isSplitEpi
- unop_mono_iff
- unop_mono_of_epi

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).