[Merged by Bors] - feat(Bicategory/Functor/Strict): add `StrictPseudofunctor` by callesonne · Pull Request #30132 · leanprover-community/mathlib4

callesonne · 2025-10-02T17:10:30Z

This PR adds the notion of a strict pseudofunctor, where the coherence isomorphisms are equalities. This will be useful for #25561 where I define the bicategory of groupoids.

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

github-actions · 2025-10-02T17:11:35Z

PR summary b7543c7cba

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ StrictPseudofunctor
+ StrictPseudofunctorCore
+ StrictPseudofunctorPreCore
+ comp
+ id
+ mk'
+ mk''
+ toFunctor

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

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean

…ories (#30134) This PR moves around some files in preparation for #30132, which introduces the notion of "strict" pseudofunctors. I want to add this new definition to the file `Bicategory/Functor/Strict.lean`, which already contains API for pseudofunctors *between* strict bicategories. My addition is about strict pseudofunctors between arbitrary bicategories. To make the distinction more clear I have decided to rearrange the file structure slightly. First I created a folder `Bicategory/Strict/` to which I move the file `Bicategory/Strict.lean` (as `Bicategory/Strict/Basic.lean`). Then I move the current file `Bicategory/Functor/Strict.lean` to `Bicategory/Strict/Pseudofunctor.lean` as I believe this fits better with the contents of the file. Then the name `Bicategory/Functor/Strict.lean` is freed up to contain the notion of a "strict" pseudofunctor in the upcoming #30132.

mathlib4-dependent-issues-bot · 2025-10-02T18:23:11Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Bicategory/Strict): move around files related to strict bicategories #30134~~
By Dependent Issues (🤖). Happy coding!

…o isStrict

Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean

…ories (leanprover-community#30134) This PR moves around some files in preparation for leanprover-community#30132, which introduces the notion of "strict" pseudofunctors. I want to add this new definition to the file `Bicategory/Functor/Strict.lean`, which already contains API for pseudofunctors *between* strict bicategories. My addition is about strict pseudofunctors between arbitrary bicategories. To make the distinction more clear I have decided to rearrange the file structure slightly. First I created a folder `Bicategory/Strict/` to which I move the file `Bicategory/Strict.lean` (as `Bicategory/Strict/Basic.lean`). Then I move the current file `Bicategory/Functor/Strict.lean` to `Bicategory/Strict/Pseudofunctor.lean` as I believe this fits better with the contents of the file. Then the name `Bicategory/Functor/Strict.lean` is freed up to contain the notion of a "strict" pseudofunctor in the upcoming leanprover-community#30132.

mathlib4-merge-conflict-bot · 2025-10-13T21:55:08Z

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

…o isStrict

callesonne · 2025-10-25T14:35:03Z

I noticed that @robin-carlier has added StrictlyUnitary.lean so I ditched the approach with IsStrict and instead copied the approach taken in that file.

mathlib4-merge-conflict-bot · 2025-11-19T08:11:11Z

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

…o isStrict

dagurtomas · 2025-11-19T17:17:41Z

Thanks!

maintainer merge

github-actions · 2025-11-19T17:17:55Z

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

Mathlib/CategoryTheory/Bicategory/Functor/StrictPseudofunctor.lean

…lean Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Mathlib/CategoryTheory/Bicategory/Functor/StrictPseudofunctor.lean

joelriou · 2025-11-23T14:04:01Z

Thanks!

bors merge

This PR adds the notion of a strict pseudofunctor, where the coherence isomorphisms are equalities. This will be useful for #25561 where I define the bicategory of groupoids.

mathlib-bors · 2025-11-23T14:23:22Z

Pull request successfully merged into master.

Build succeeded:

add files and rearrange

7bb9706

callesonne added the t-category-theory Category theory label Oct 2, 2025

github-actions bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label Oct 2, 2025

joelriou reviewed Oct 2, 2025

View reviewed changes

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

callesonne mentioned this pull request Oct 2, 2025

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

Closed

cat_DISCH

7f72c1f

mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Oct 2, 2025

Merge branch 'master' of github.com:leanprover-community/mathlib4 int…

3f05522

…o isStrict

github-actions bot removed the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label Oct 2, 2025

callesonne added 4 commits October 2, 2025 19:52

file

a94eb5c

docs

6825325

docs again

f036c05

mk_all

0fa6d2d

joelriou reviewed Oct 3, 2025

View reviewed changes

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

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

joelriou requested a review from robin-carlier October 3, 2025 19:10

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 13, 2025

Merge branch 'master' of github.com:leanprover-community/mathlib4 int…

49af11b

…o isStrict

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 25, 2025

callesonne added 2 commits October 25, 2025 15:30

fix

b2b69d3

docs

8f25e4c

add precore

dd15806

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

rename and fix by cat_rfl

28c233c

callesonne removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 11, 2025

callesonne added 3 commits November 11, 2025 12:16

Merge branch 'isStrict' of github.com:callesonne/mathlib4 into isStrict

ffd1546

import fix

7f96b52

rfl_cat

27cef16

leanprover-community-bot-assistant assigned robin-carlier Nov 15, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

callesonne added 2 commits November 19, 2025 08:53

Merge branch 'master' of github.com:leanprover-community/mathlib4 int…

06319f9

…o isStrict

mk

5f72fac

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

fix

e2baf5b

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

joelriou reviewed Nov 19, 2025

View reviewed changes

Mathlib/CategoryTheory/Bicategory/Functor/StrictPseudofunctor.lean Show resolved Hide resolved

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

Update Mathlib/CategoryTheory/Bicategory/Functor/StrictPseudofunctor.…

6d98bbc

…lean Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

callesonne removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 19, 2025

jcommelin reviewed Nov 21, 2025

View reviewed changes

Mathlib/CategoryTheory/Bicategory/Functor/StrictPseudofunctor.lean Show resolved Hide resolved

callesonne added 2 commits November 21, 2025 14:29

add simps

445c72a

Merge branch 'isStrict' of github.com:callesonne/mathlib4 into isStrict

02e3b1d

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Nov 23, 2025

mathlib-bors bot changed the title ~~feat(Bicategory/Functor/Strict): add StrictPseudofunctor~~ [Merged by Bors] - feat(Bicategory/Functor/Strict): add StrictPseudofunctor Nov 23, 2025

mathlib-bors bot closed this Nov 23, 2025

callesonne deleted the isStrict branch December 4, 2025 09:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Bicategory/Functor/Strict): add `StrictPseudofunctor`#30132

[Merged by Bors] - feat(Bicategory/Functor/Strict): add `StrictPseudofunctor`#30132
callesonne wants to merge 24 commits intoleanprover-community:masterfrom
callesonne:isStrict

callesonne commented Oct 2, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Oct 2, 2025 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Oct 2, 2025

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Oct 13, 2025

Uh oh!

callesonne commented Oct 25, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

dagurtomas commented Nov 19, 2025

Uh oh!

github-actions bot commented Nov 19, 2025

Uh oh!

Uh oh!

Uh oh!

joelriou commented Nov 23, 2025

Uh oh!

mathlib-bors bot commented Nov 23, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

Conversation

callesonne commented Oct 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary b7543c7cba

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Oct 2, 2025

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Oct 13, 2025

Uh oh!

callesonne commented Oct 25, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

dagurtomas commented Nov 19, 2025

Uh oh!

github-actions bot commented Nov 19, 2025

Uh oh!

Uh oh!

Uh oh!

joelriou commented Nov 23, 2025

Uh oh!

mathlib-bors bot commented Nov 23, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

callesonne commented Oct 2, 2025 •

edited

Loading

github-actions bot commented Oct 2, 2025 •

edited

Loading