feat(CategoryTheory/Shift): shifted morphisms in the opposite category

[joelriou]

When C is a triangulated category, we introduce a bijection ShiftedHom.opEquiv which identifies X ⟶ Y⟦n⟧ and op Y ⟶ (op X)⟦n⟧ for any objects X and Y in C, and n : ℤ.
Along with the compatibilities that are obtained, this shall be the main ingredient in the construction of the (contravariant) long exact sequence of Ext in abelian categories #15092.

---

[github-actions]

PR summary ce01e1cc6c

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Triangulated.Yoneda	1238	1240	+2 (+0.16%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences	1
Mathlib.CategoryTheory.Triangulated.Yoneda	2
Mathlib.CategoryTheory.Shift.ShiftedHomOpposite	1071

---

Declarations diff

+ Hom.opEquiv
+ instance (B : C) : (preadditiveYoneda.obj B).ShiftSequence ℤ
+ opEquiv
+ opEquiv'
+ opEquiv'_add_symm
+ opEquiv'_apply
+ opEquiv'_symm_add
+ opEquiv'_symm_apply
+ opEquiv'_symm_comp
+ opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift
+ opEquiv'_zero_add_symm
+ opEquiv_symm_add
+ opEquiv_symm_apply
+ opEquiv_symm_apply_comp
+ opEquiv_symm_comp
+ opShiftFunctorEquivalence_unitIso_hom_app_eq
+ opShiftFunctorEquivalence_unitIso_inv_app_eq
+ opShiftFunctorEquivalence_zero_unitIso_hom_app
+ opShiftFunctorEquivalence_zero_unitIso_inv_app
+ preadditiveYoneda_homologySequenceδ_apply
+ preadditiveYoneda_shiftMap_apply
+ shiftFunctorCompIsoId_add'_hom_app
+ shiftFunctorCompIsoId_add'_inv_app
+ shiftFunctorCompIsoId_zero_zero_hom_app
+ shiftFunctorCompIsoId_zero_zero_inv_app

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.