feat(CategoryTheory/Bicategory/Span): bicategories of spans

[robin-carlier]

In this PR, we extend the constructions from #39536 to a bicategory structure on Spans C Wₗ Wᵣ, which is a type alias for C, where the 1-morphisms are spans in C with left leg satisfying Wₗ and the right leg satisfies Wᵣ.

From SymmMonCoherence

---

• depends on: [Merged by Bors] - feat(CategoryTheory/Bicategory): Spans with left and right legs satisfying given morphism properties #39536

[github-actions]

PR summary 47cc982d1f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ Spans
+ apexIso
+ apexIso_refl
+ associator
+ associator_hom_hom_πᵣ_πᵣ
+ associator_hom_hom_πᵣ_πₗ
+ associator_hom_hom_πₗ
+ associator_inv_hom_πᵣ
+ associator_inv_hom_πₗ_πᵣ
+ associator_inv_hom_πₗ_πₗ
+ compLift
+ compLiftApex
+ compLiftApex_πᵣ
+ compLiftApex_πₗ
+ compLift_hom_πᵣ
+ compLift_hom_πₗ
+ compPullbackCone
+ compPullbackCone_fst
+ compPullbackCone_snd
+ comp_comm
+ comp_hom_ext_apex
+ comp_l
+ comp_r
+ eqToHom_hom
+ hom_inv_id_hom
+ hom₂_comp_hom
+ hom₂_ext
+ hom₂_id_hom
+ id_apex
+ id_l
+ id_r
+ instance (S : X ⟶ Y) : IsIso (πᵣ (𝟙 _) S) := by
+ instance (S : X ⟶ Y) : IsIso (πₗ S (𝟙 _))
+ instance : Bicategory (Spans C Wₗ Wᵣ)
+ instance : CategoryStruct (Spans C Wₗ Wᵣ)
+ instance : IsIso (𝟙 X:).l := by dsimp; infer_instance
+ instance : IsIso (𝟙 X:).r := by dsimp; infer_instance
+ instance {S S' : X ⟶ Y} (e : S ⟶ S') [IsIso e] : IsIso e.hom
+ instance {X Y : Spans C Wₗ Wᵣ} : Category (X ⟶ Y)
+ inv_hom
+ inv_hom_id_hom
+ isLimitCompPullbackCone
+ leftUnitor
+ leftUnitor_hom_hom
+ leftUnitor_inv_hom_πᵣ
+ leftUnitor_inv_hom_πₗ
+ mkHom
+ mkHom₂
+ mkIso₂
+ rightUnitor
+ rightUnitor_hom_hom
+ rightUnitor_inv_hom_πᵣ
+ rightUnitor_inv_hom_πₗ
+ whiskerLeft_hom_πᵣ
+ whiskerLeft_hom_πₗ
+ whiskerRight_hom_πᵣ
+ whiskerRight_hom_πₗ
+ πᵣ
+ πₗ

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 47cc982).

• +103 new declarations
• −0 removed declarations

+CategoryTheory.Span.Hom.hom.hcongr_9
+CategoryTheory.Span.Spans
+CategoryTheory.Span.Spans.apexIso
+CategoryTheory.Span.Spans.apexIso_hom
+CategoryTheory.Span.Spans.apexIso_inv
+CategoryTheory.Span.Spans.apexIso_refl
+CategoryTheory.Span.Spans.associator
+CategoryTheory.Span.Spans.associator_hom_hom_πᵣ_πᵣ
+CategoryTheory.Span.Spans.associator_hom_hom_πᵣ_πᵣ_assoc
+CategoryTheory.Span.Spans.associator_hom_hom_πᵣ_πₗ
+CategoryTheory.Span.Spans.associator_hom_hom_πᵣ_πₗ_assoc
+CategoryTheory.Span.Spans.associator_hom_hom_πₗ
+CategoryTheory.Span.Spans.associator_hom_hom_πₗ_assoc
+CategoryTheory.Span.Spans.associator_inv_hom_πᵣ
+CategoryTheory.Span.Spans.associator_inv_hom_πᵣ_assoc
+CategoryTheory.Span.Spans.associator_inv_hom_πₗ_πᵣ
+CategoryTheory.Span.Spans.associator_inv_hom_πₗ_πᵣ_assoc
+CategoryTheory.Span.Spans.associator_inv_hom_πₗ_πₗ
+CategoryTheory.Span.Spans.associator_inv_hom_πₗ_πₗ_assoc
+CategoryTheory.Span.Spans.casesOn
+CategoryTheory.Span.Spans.compLift
+CategoryTheory.Span.Spans.compLift.congr_simp
+CategoryTheory.Span.Spans.compLiftApex
+CategoryTheory.Span.Spans.compLiftApex.congr_simp
+CategoryTheory.Span.Spans.compLiftApex_πᵣ
+CategoryTheory.Span.Spans.compLiftApex_πᵣ_assoc
+CategoryTheory.Span.Spans.compLiftApex_πₗ
+CategoryTheory.Span.Spans.compLiftApex_πₗ_assoc
+CategoryTheory.Span.Spans.compLift_hom
+CategoryTheory.Span.Spans.compLift_hom_πᵣ
+CategoryTheory.Span.Spans.compLift_hom_πₗ
+CategoryTheory.Span.Spans.compPullbackCone
+CategoryTheory.Span.Spans.compPullbackCone_fst
+CategoryTheory.Span.Spans.compPullbackCone_pt
+CategoryTheory.Span.Spans.compPullbackCone_snd
+CategoryTheory.Span.Spans.comp_comm
+CategoryTheory.Span.Spans.comp_comm_assoc
+CategoryTheory.Span.Spans.comp_hom_ext_apex
+CategoryTheory.Span.Spans.comp_hom_ext_apex_iff
+CategoryTheory.Span.Spans.comp_l
+CategoryTheory.Span.Spans.comp_l_assoc
+CategoryTheory.Span.Spans.comp_r
+CategoryTheory.Span.Spans.comp_r_assoc
+CategoryTheory.Span.Spans.ctorIdx
+CategoryTheory.Span.Spans.eqToHom_hom
+CategoryTheory.Span.Spans.hom_inv_id_hom
+CategoryTheory.Span.Spans.hom_inv_id_hom_assoc
+CategoryTheory.Span.Spans.hom₂_comp_hom
+CategoryTheory.Span.Spans.hom₂_ext
+CategoryTheory.Span.Spans.hom₂_ext_iff
+CategoryTheory.Span.Spans.hom₂_id_hom
+CategoryTheory.Span.Spans.id_apex
+CategoryTheory.Span.Spans.id_l
+CategoryTheory.Span.Spans.id_r
+CategoryTheory.Span.Spans.instBicategory
+CategoryTheory.Span.Spans.instCategoryHom
+CategoryTheory.Span.Spans.instCategoryStruct
+CategoryTheory.Span.Spans.instIsIsoHomOfHom
+CategoryTheory.Span.Spans.instIsIsoLId
+CategoryTheory.Span.Spans.instIsIsoRId
+CategoryTheory.Span.Spans.instIsIsoπᵣId
+CategoryTheory.Span.Spans.instIsIsoπₗId
+CategoryTheory.Span.Spans.inv_hom
+CategoryTheory.Span.Spans.inv_hom_id_hom
+CategoryTheory.Span.Spans.inv_hom_id_hom_assoc
+CategoryTheory.Span.Spans.isLimitCompPullbackCone
+CategoryTheory.Span.Spans.leftUnitor
+CategoryTheory.Span.Spans.leftUnitor_hom_hom
+CategoryTheory.Span.Spans.leftUnitor_inv_hom_πᵣ
+CategoryTheory.Span.Spans.leftUnitor_inv_hom_πₗ
+CategoryTheory.Span.Spans.mk
+CategoryTheory.Span.Spans.mk.inj
+CategoryTheory.Span.Spans.mk.injEq
+CategoryTheory.Span.Spans.mk.noConfusion
+CategoryTheory.Span.Spans.mk.sizeOf_spec
+CategoryTheory.Span.Spans.mkHom
+CategoryTheory.Span.Spans.mkHom₂
+CategoryTheory.Span.Spans.mkHom₂_hom
+CategoryTheory.Span.Spans.mkIso₂
+CategoryTheory.Span.Spans.noConfusion
+CategoryTheory.Span.Spans.noConfusionType
+CategoryTheory.Span.Spans.of
+CategoryTheory.Span.Spans.rec
+CategoryTheory.Span.Spans.recOn
+CategoryTheory.Span.Spans.rightUnitor
+CategoryTheory.Span.Spans.rightUnitor_hom_hom
+CategoryTheory.Span.Spans.rightUnitor_inv_hom_πᵣ
+CategoryTheory.Span.Spans.rightUnitor_inv_hom_πᵣ_assoc
+CategoryTheory.Span.Spans.rightUnitor_inv_hom_πₗ
+CategoryTheory.Span.Spans.rightUnitor_inv_hom_πₗ_assoc
+CategoryTheory.Span.Spans.whiskerLeft_hom_πᵣ
+CategoryTheory.Span.Spans.whiskerLeft_hom_πᵣ_assoc
+CategoryTheory.Span.Spans.whiskerLeft_hom_πₗ
+CategoryTheory.Span.Spans.whiskerLeft_hom_πₗ_assoc
+CategoryTheory.Span.Spans.whiskerRight_hom_πᵣ
+CategoryTheory.Span.Spans.whiskerRight_hom_πᵣ_assoc
+CategoryTheory.Span.Spans.whiskerRight_hom_πₗ
+CategoryTheory.Span.Spans.whiskerRight_hom_πₗ_assoc
+CategoryTheory.Span.Spans.πᵣ
+CategoryTheory.Span.Spans.πₗ
+CategoryTheory.Span.apex.hcongr_7
+CategoryTheory.Span.l.hcongr_7
+CategoryTheory.Span.r.hcongr_7

---

Increase in strong tech debt: (relative, absolute) = (6.00, 0.00)

Current number	Change	Type (strong)
5780	6	backward.isDefEq.respectTransparency

No changes to weak technical debt.

Current commit 47cc982d1f
Reference commit c0ba100fa0

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory/Bicategory): Spans with left and right legs satisfying given morphism properties #39536
  By Dependent Issues (🤖). Happy coding!

[joelriou]

Could we make apex implicit here?

[joelriou]

Should this be Span?

[robin-carlier]

The problem is that Span is already taken above (Span Wₗ Wᵣ c₁ c₂ is the type of spans from c₁ to c₂ with left leg satisfying Wₗ and right leg satisfying Wᵣ)
SpanBicat is an option as well..

[joelriou]

Ah, then SpanBicat would be better IMO.