Rebase experimental onto latest master

[andreasabel]

• [Refractor] contradiction over ⊥-elim in ¬-not def ([Refractor] contradiction over ⊥-elim in ¬-not def #2661)
• [Refractor] contradiction over ⊥-elim ([Refractor] contradiction over ⊥-elim src/Data/Vec/Functional/Properties.agda #2664)
• [Import] Function.Nary...Function* ([Import] Function.Nary...Function* #2641)
• [Import] Reflection ([Import] Reflection #2643)
• fix: one line in "Algebra.Bundles.Raw" is redundant #2680 ([ fix ] remove redundant import #2681)
• [Refractor] contradiction over ⊥-elim in Data.*.Relation.Binary.Lex.* ([Refractor] contradiction over ⊥-elim in Data.*.Relation.Binary.Lex.* #2671)
• [Refactor] imports to use Relation.Nullary.Irrelevant ([Refactor] imports to use Relation.Nullary.Irrelevant #2676)
• [ add ] wellfoundedness of Relation.Binary.Construct.Add.Infimum.Strict ([ add ] wellfoundedness of Relation.Binary.Construct.Add.Infimum.Strict #2683)
• refactor: fix lemma names ([ refactor ] Rename Algebra.Lattice.Properties.BooleanAlgebra.{⊥≉⊤,⊤≉⊥} #2686)
• [ refactor ] deprecate Algebra.Structures.IsGroup.{uniqueˡ-⁻¹|uniqueʳ-⁻¹} with knock-ons for Algebra.Module.* ([ refactor ] deprecate Algebra.Structures.IsGroup.{uniqueˡ-⁻¹|uniqueʳ-⁻¹} with knock-ons for Algebra.Module.* #2571)
• [ fix ] issue The explanation of Bundle.Raw seems to have a typo #2698, plus corrects naming convention ([ fix ] documentation of Algebra.Bundles.Raw in README.Design.Hierarchies #2699)
• [ fix ] attach fixity to the new declaration of Function.Base.case_returning_of_ ([ fix ] attach fixity to the new declaration of Function.Base.case_returning_of_ #2694)
• Add properties of zipWith to Pointwise ([add] properties of zipWith to Pointwise (Data.Vec) #2703)
• fix: redundant import ([ fix ] redundant import in Data.Fin.Base #2707)
• Add/fix RightInverse for dependent products (Add/fix RightInverse for dependent products #2706)
• [add] Update PartialSetoid reasoning ([add] Update PartialSetoid reasoning #2689)
• [ add ] obvious lemma about self-contradiction to Relation.Nullary.Negation.Core ([ add ] obvious lemma about self-contradiction to Relation.Nullary.Negation.Core #2693)
• fix bug Relation.Binary.Morphism.Bundles (Fix bug in Relation.Binary.Morphism.Bundles usage #2713)
• Bump Haskell CI to GHCs 9.12.2 9.10.2 9.6.7 (ghc 9.12.2 #2714)
• Fix #7669: positivity checker: compute function arity up to def. eq. agda#7674 eta-expand fields in record expression
• Workaround for Agda 2.7.0 (and lower, I suppose)