[Merged by Bors] - feat(CategoryTheory): pseudofunctors to Cat by joelriou · Pull Request #25971 · leanprover-community/mathlib4

joelriou · 2025-06-16T18:43:13Z

This PR adds convenience lemmas for pseudofunctors to Cat, mostly using the to_app attribute. The simp set for the to_app attribute is extended in order to take into account that in Cat, associators and unitors induce identities.

depends on: [Merged by Bors] - chore(Bicategory/Strict): move around files related to strict bicategories #30134

This PR continues the work from #24384.

Original PR: #24384

…e-cat

joelriou · 2025-06-16T18:43:15Z

Comments from Original PR #24384

This section contains 1 comment(s) from the original PR, excluding bot comments.

@github-actions (2025-04-26 10:22 UTC):

PR summary db52f0992d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Bicategory.Functor.Cat` (new file)	367

Declarations diff

+ mapComp'_comp_id_hom_app
+ mapComp'_comp_id_inv_app
+ mapComp'_hom_app_comp_mapComp'_hom_app_map_obj
+ mapComp'_hom_app_comp_map_map_mapComp'_hom_app
+ mapComp'_hom_naturality
+ mapComp'_id_comp_hom_app
+ mapComp'_id_comp_inv_app
+ mapComp'_inv_app_comp_mapComp'_hom_app
+ mapComp'_inv_app_map_obj_comp_mapComp'_inv_app
+ mapComp'_inv_naturality
+ mapComp'_naturality_1
+ mapComp'_naturality_2
+ mapComp'₀₁₃_hom_app
+ mapComp'₀₁₃_inv_app
+ mapId'_hom_naturality
+ mapId'_inv_naturality
+ map_map_mapComp'_inv_app_comp_mapComp'_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.

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

github-actions · 2025-06-16T18:44:34Z

PR summary c4b611e415

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Bicategory.Functor.Cat` (new file)	387

Declarations diff

+ mapComp'_comp_id_hom
+ mapComp'_comp_id_inv
+ mapComp'_hom_naturality
+ mapComp'_id_comp_hom
+ mapComp'_id_comp_inv
+ mapComp'_inv_naturality
+ mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv
+ mapComp'_naturality_1
+ mapComp'_naturality_2
+ mapComp'₀₁₃_hom
+ mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom
+ mapComp'₀₁₃_inv
+ mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom
+ mapComp'₀₂₃_hom
+ mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight
+ mapComp'₀₂₃_inv
+ mapId'_hom_naturality
+ mapId'_inv_naturality
+ whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv

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

…comp-prime-cat

Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean

callesonne

LGTM modulo this one comment. Thanks!

Co-authored-by: Calle Sönne <calle.sonne@gmail.com>

callesonne

~~(forgot to approve)~~ I seem to have gotten confused by the display / permission changes?

Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean

yuma-mizuno

LGTM modulo few comments.

Mathlib/Tactic/CategoryTheory/ToApp.lean

MathlibTest/CategoryTheory/ToApp.lean

Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean

Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean

Co-authored-by: Yuma Mizuno <mizuno.y.aj@gmail.com>

…mp-prime-cat

Co-authored-by: Yuma Mizuno <mizuno.y.aj@gmail.com>

robin-carlier

Only a nitpick about universe-level mvars, but otherwise looks good! Thanks @yuma-mizuno and @callesonne and @chrisflav for the reviews as well!

maintainer delegate

robin-carlier · 2025-10-12T12:14:30Z

Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean

+-- this linter rejects `@[to_app (attr := reassoc)]`
+set_option linter.style.commandStart false


Did you report this on Zulip?

Thanks for the suggestion #mathlib4 > linter commandStart does not like @[to_app (attr := reassoc) @ 💬

Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean

github-actions · 2025-10-12T12:24:04Z

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

riccardobrasca · 2025-10-12T12:42:44Z

Thanks!

bors d+

mathlib-bors · 2025-10-12T12:42:46Z

✌️ joelriou 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: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>

…mp-prime-cat

joelriou · 2025-10-12T14:19:41Z

Thanks!

bors merge

This PR adds convenience lemmas for pseudofunctors to `Cat`, mostly using the `to_app` attribute. The simp set for the `to_app` attribute is extended in order to take into account that in `Cat`, associators and unitors induce identities.

mathlib-bors · 2025-10-12T14:36:48Z

Pull request successfully merged into master.

Build succeeded:

This PR adds convenience lemmas for pseudofunctors to `Cat`, mostly using the `to_app` attribute. The simp set for the `to_app` attribute is extended in order to take into account that in `Cat`, associators and unitors induce identities.

joelriou added 10 commits April 26, 2025 10:18

feat(CategoryTheory): pseudofunctors from strict bicategories

4913881

better names

430466b

cleaning up

6d3eca6

whitespace

74dc8c5

cleaning up

6529163

better lemmas

45d4532

feat(CategoryTheory): pseudofunctors to Cat

050a27a

more lemmas

4ca7538

fix

fdfad5b

Merge remote-tracking branch 'origin' into pseudofunctor-mapcomp-prim…

a11351e

…e-cat

joelriou mentioned this pull request Jun 16, 2025

feat(CategoryTheory): pseudofunctors to Cat #24384

Closed

1 task

github-actions bot added the t-category-theory Category theory label Jun 16, 2025

This was referenced Jun 16, 2025

feat(CategoryTheory): effectiveness of descent #24434

Open

feat(CategoryTheory): descent of morphisms for a pseudofunctor #24411

Closed

joelriou added awaiting-author A reviewer has asked the author a question or requested changes. WIP Work in progress labels Jun 16, 2025

joelriou added 4 commits June 18, 2025 13:09

Merge remote-tracking branch 'upstream/master' into pseudofunctor-map…

da748f4

…comp-prime-cat

used/fixed to_app

006d77d

fixed tests

29f1496

fixed imports

c97b420

joelriou removed awaiting-author A reviewer has asked the author a question or requested changes. WIP Work in progress labels Jun 18, 2025

callesonne reviewed Jun 18, 2025

View reviewed changes

Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean Outdated Show resolved Hide resolved

callesonne approved these changes Jun 18, 2025

View reviewed changes

Update Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean

46c29d4

Co-authored-by: Calle Sönne <calle.sonne@gmail.com>

callesonne approved these changes Jun 18, 2025

View reviewed changes

chrisflav reviewed Jun 18, 2025

View reviewed changes

Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean Show resolved Hide resolved

Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean Show resolved Hide resolved

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 18, 2025

This was referenced Oct 4, 2025

[Merged by Bors] - feat(CategoryTheory/Sites): descent data #30189

Closed

[Merged by Bors] - feat(CategoryTheory/Sites): functoriality of descent data #30190

Closed

yuma-mizuno approved these changes Oct 4, 2025

View reviewed changes

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 4, 2025

joelriou and others added 6 commits October 8, 2025 20:15

Update Mathlib/Tactic/CategoryTheory/ToApp.lean

c266eb8

Co-authored-by: Yuma Mizuno <mizuno.y.aj@gmail.com>

Merge remote-tracking branch 'origin/master' into pseudofunctor-mapco…

5aa7e9c

…mp-prime-cat

Update Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean

1e2b4da

Co-authored-by: Yuma Mizuno <mizuno.y.aj@gmail.com>

Update Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean

e99f268

Co-authored-by: Yuma Mizuno <mizuno.y.aj@gmail.com>

whitespace

279bbb9

suggestion by yuma-mizuno

d0062bc

joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 8, 2025

robin-carlier reviewed Oct 12, 2025

View reviewed changes

robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 12, 2025

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 12, 2025

joelriou and others added 3 commits October 12, 2025 15:35

Update Mathlib/CategoryTheory/Bicategory/Functor/Cat.lean

8ce0607

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

Merge remote-tracking branch 'origin/master' into pseudofunctor-mapco…

955653f

…mp-prime-cat

fixing to_app (attr:=...) syntax

8771d68

ghost added the ready-to-merge This PR has been sent to bors. label Oct 12, 2025

mathlib-bors bot changed the title ~~feat(CategoryTheory): pseudofunctors to Cat~~ [Merged by Bors] - feat(CategoryTheory): pseudofunctors to Cat Oct 12, 2025

mathlib-bors bot closed this Oct 12, 2025

		-- this linter rejects `@[to_app (attr := reassoc)]`
		set_option linter.style.commandStart false

Conversation

joelriou commented Jun 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

joelriou commented Jun 16, 2025

Comments from Original PR #24384

PR summary db52f0992d

Import changes for modified files

Declarations diff

Uh oh!

github-actions bot commented Jun 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c4b611e415

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

callesonne left a comment

Choose a reason for hiding this comment

Uh oh!

callesonne left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

yuma-mizuno left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

robin-carlier left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

robin-carlier Oct 12, 2025

Choose a reason for hiding this comment

Uh oh!

joelriou Oct 12, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Oct 12, 2025

Uh oh!

riccardobrasca commented Oct 12, 2025

Uh oh!

mathlib-bors bot commented Oct 12, 2025

Uh oh!

joelriou commented Oct 12, 2025

Uh oh!

mathlib-bors bot commented Oct 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

joelriou commented Jun 16, 2025 •

edited

Loading

github-actions bot commented Jun 16, 2025 •

edited

Loading

callesonne left a comment •

edited

Loading

robin-carlier left a comment •

edited

Loading