[Merged by Bors] - feat(CategoryTheory/Bicategory): Spans with left and right legs satisfying given morphism properties by robin-carlier · Pull Request #39536 · leanprover-community/mathlib4

robin-carlier · 2026-05-18T16:49:48Z

In this PR, we define a structure Span Wₗ Wᵣ c c' which bundles the data of spans in C from c to c' where the left map satisfies Wₗ and the right map satisfies Wᵣ. When Wₗ and Wᵣ are adequate, we define the identity span and the composition of compatible spans.

In a later pull request, this will be extended to be the 1-morphisms of a bicategory structure on a type alias of C.

From SymmMonCoherence

depends on: [Merged by Bors] - feat(CategoryTheory/MorphismProperty): HasPullbacksAgainst #39534
depends on: [Merged by Bors] - fix(CategoryTheory/MorphismProperty/Limits): change duplicate lemma #39647

github-actions · 2026-05-18T16:51:08Z

PR summary 4c9b125de5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Bicategory.Span.Basic` (new file)	687

Declarations diff

+ Hom
+ Span
+ comp
+ hom_ext
+ id
+ instance (S₁ : Span Wₗ Wᵣ c c') : Wᵣ.IsStableUnderBaseChangeAlong S₁.l
+ instance (S₁ : Span Wₗ Wᵣ c c') : Wₗ.IsStableUnderBaseChangeAlong S₁.r
+ instance : Category (Span Wₗ Wᵣ c c')
+ instance {c c' c'' : C} (S₁ : Span Wₗ Wᵣ c c') (S₂ : Span Wₗ Wᵣ c' c'') : HasPullback S₁.r S₂.l
+ mkIso

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.

No changes to strong technical debt.

No changes to weak technical debt.

mathlib-dependent-issues · 2026-05-21T11:52:39Z

This PR/issue depends on:

~~[Merged by Bors] - feat(CategoryTheory/MorphismProperty): HasPullbacksAgainst #39534~~
~~[Merged by Bors] - fix(CategoryTheory/MorphismProperty/Limits): change duplicate lemma #39647~~
By Dependent Issues (🤖). Happy coding!

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

dagurtomas

Thanks!

maintainer delegate

github-actions · 2026-05-21T20:16:22Z

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

riccardobrasca · 2026-05-23T11:17:47Z

Thanks!

bors d+

mathlib-bors · 2026-05-23T11:17:49Z

✌️ robin-carlier can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

… properties

robin-carlier · 2026-05-28T05:52:36Z

Thanks!

bors r+

…fying given morphism properties (#39536) In this PR, we define a structure `Span Wₗ Wᵣ c c'` which bundles the data of spans in `C` from `c` to `c'` where the left map satisfies `Wₗ` and the right map satisfies `Wᵣ`. When `Wₗ` and `Wᵣ` are adequate, we define the identity span and the composition of compatible spans. In a later pull request, this will be extended to be the 1-morphisms of a bicategory structure on a type alias of `C`. From [SymmMonCoherence](https://github.com/robin-carlier/SymmMonCoherence)

mathlib-bors · 2026-05-28T06:05:32Z

Pull request successfully merged into master.

Build succeeded:

…fying given morphism properties (leanprover-community#39536) In this PR, we define a structure `Span Wₗ Wᵣ c c'` which bundles the data of spans in `C` from `c` to `c'` where the left map satisfies `Wₗ` and the right map satisfies `Wᵣ`. When `Wₗ` and `Wᵣ` are adequate, we define the identity span and the composition of compatible spans. In a later pull request, this will be extended to be the 1-morphisms of a bicategory structure on a type alias of `C`. From [SymmMonCoherence](https://github.com/robin-carlier/SymmMonCoherence)

robin-carlier added 9 commits May 13, 2026 19:38

WIP

31effdc

WIP

f6c82d6

fix: fix bad name

a8e8ab7

fix: typo in docstring

22853d3

WIP

939c5d7

WIP

8e7d4be

remove projections

383cdcf

feat: lint and add a section

3759764

chore:split

29588d7

github-actions Bot added the t-category-theory Category theory label May 18, 2026

robin-carlier mentioned this pull request May 18, 2026

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

Open

1 task

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 18, 2026

fix: lake exe mk_all

9fb1bb9

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 20, 2026

robin-carlier added 5 commits May 21, 2026 10:46

fix: change incorrectly named lemma

9860e46

fix: fix docstrings

ba0f3f7

fix: fix docstrings again

cd9b813

Merge branch 'fix_name_hasPullbackAgainstTop_iff' into spans

ebc78cf

fix: replace unicode char

14cc6e2

robin-carlier commented May 21, 2026

View reviewed changes

Comment thread Mathlib/CategoryTheory/Bicategory/Span/Basic.lean Outdated

Comment thread Mathlib/CategoryTheory/Bicategory/Span/Basic.lean Outdated

Comment thread Mathlib/CategoryTheory/Bicategory/Span/Basic.lean Outdated

Apply suggestions from code review

451236e

Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

dagurtomas reviewed May 21, 2026

View reviewed changes

Comment thread Mathlib/CategoryTheory/Bicategory/Span/Basic.lean Outdated

Comment thread Mathlib/CategoryTheory/Bicategory/Span/Basic.lean Outdated

Comment thread Mathlib/CategoryTheory/Bicategory/Span/Basic.lean Outdated

Comment thread Mathlib/CategoryTheory/Bicategory/Span/Basic.lean Outdated

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 21, 2026

mathlib-triage Bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 23, 2026

robin-carlier and others added 3 commits May 27, 2026 22:05

Apply suggestions from code review

4e54f65

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>

doc: expand module docstring to explain the condition on the morphism…

9a22caf

… properties

Merge remote-tracking branch 'upstream/master' into spans

4c9b125

robin-carlier added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 27, 2026

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 27, 2026

mathlib-bors Bot changed the title ~~feat(CategoryTheory/Bicategory): Spans with left and right legs satisfying given morphism properties~~ [Merged by Bors] - feat(CategoryTheory/Bicategory): Spans with left and right legs satisfying given morphism properties May 28, 2026

mathlib-bors Bot closed this May 28, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

[Merged by Bors] - feat(CategoryTheory/Bicategory): Spans with left and right legs satisfying given morphism properties#39536
robin-carlier wants to merge 19 commits into
leanprover-community:masterfrom
robin-carlier:spans

robin-carlier commented May 18, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented May 18, 2026 •

edited

Loading

Declarations diff

Uh oh!

mathlib-dependent-issues Bot commented May 21, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

dagurtomas left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented May 21, 2026

Uh oh!

riccardobrasca commented May 23, 2026

Uh oh!

mathlib-bors Bot commented May 23, 2026

Uh oh!

robin-carlier commented May 28, 2026

Uh oh!

mathlib-bors Bot commented May 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

robin-carlier commented May 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 4c9b125de5

Import changes for modified files

Declarations diff

Uh oh!

mathlib-dependent-issues Bot commented May 21, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

dagurtomas left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented May 21, 2026

Uh oh!

riccardobrasca commented May 23, 2026

Uh oh!

mathlib-bors Bot commented May 23, 2026

Uh oh!

robin-carlier commented May 28, 2026

Uh oh!

mathlib-bors Bot commented May 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

robin-carlier commented May 18, 2026 •

edited

Loading

github-actions Bot commented May 18, 2026 •

edited

Loading