feat(CategoryTheory/Sites): morphisms and homotopies of 1-hypercovers

[chrisflav]

We define refinement morphisms and homotopies between morphisms of (pre-)-1-hypercovers. As a sanity check, we show that

• homotopic maps induce the same map on the corresponding multiequalizers
• the category of 1-hypercovers is cofiltered up to homotopies, i.e. for any two refinement morphisms there exists a refinement from the left such that both compositions are homotopic.

In the next PR, we define the (homotopy) category of 1-hypercovers with refinement morphisms modulo homotopy. This will be a cofiltered category and taking a colimit over these will give a second approach to sheafification.

---

[github-actions]

PR summary 22cd4a1164

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Hom
+ Hom.comp
+ Hom.id
+ Hom.mapMultiforkOfIsLimit
+ Hom.mapMultiforkOfIsLimit_ι
+ Hom.s₁'
+ Homotopy
+ Homotopy.mapMultiforkOfIsLimit_eq
+ Presieve.bind_ofArrows_le_bindOfArrows
+ cylinderHom
+ cylinderHomotopy
+ cylinderX
+ cylinderf
+ instance : Category (PreOneHypercover S)
+ sieve₀_cylinder
+ sieve₁'_cylinder
+ toPullback_cylinder
++ bindOfArrows
++ cylinder
++ exists_nonempty_homotopy

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/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).

[chrisflav]

This PR also seems to suffer from https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Failing.20CI/with/525466176.

[joelriou]

Could you introduce an abbrev OneHypercover.Hom?