Bicategory (Is1Cat compatible design) #2272

patrick-nicodemus · 2025-04-01T16:13:22Z

This PR defines a wild bicategory. This is a rewrite of the previous PR, because my original definition of a 1Bicat was too far from the definition of a 1Cat, making it a lot of work to port work using 1Cats to use 1Bicats instead; the new definition of a 1Bicat mimics 1Cat as closely as possible.
Also, with my original definition using Is0Bifunctor there are two different ways to whisker a 2-cell with a 1-cell that are not in any way related, and this seems like a potential pitfall.

On the other hand, the definition of a Bicategory is more of a departure from the current definition of a (2,1)-category, in that it assumes that the associator is natural as a functor on (a $-> b) * (b $-> c) * (c $-> d) rather than being natural in each argument separately. This definition is more complex because it uses products and uncurrying, but I preferred the style, and there's not as much material in the library for (2,1)-cats as there is for 1-cats so refactoring is not as much of an issue.

The first commit defines a 1-bicategory (which is a wild 1-category without the requirement that 2-cells are invertible) and a bicategory; it refactors the definition of (2,1)-category to extend bicategory; all (2,1)-categories (the path groupoid of a type, the universe Type, pType) are rewritten as bicategories. While writing the proofs that pType is a bicategory I took care to try and reuse the same proofs for Type in many places. A few helper lemmas in constructing the (2,1)-category of paths are extracted and put in PathGroupoid.v. Notation is introduced for vertical pasting.
In the second commit, a definition is given to upgrade a 1-bicategory to a 1-category when 2-cells are invertible; all near-duplicate definitions from the first commit are deduplicated.
The third commit better integrates AreInverse into the library by rewriting Is1Gpd to depend on AreInverse.

jdchristensen · 2025-04-27T12:44:52Z

I haven't had time to look at this. I was hoping @Alizter might get a chance, but if not, I'll add it to my list.

Alizter · 2025-04-27T14:08:28Z

I have been very busy these past few weeks unfortunately and didn't have the brain-power to think about this.

jdchristensen

I've made a first pass through. Feel free to do an interactive rebase and a force push to move the changes from the "undid change to master" commit into the earlier commit(s), but it'll be easier to review if other changes are made as additional commits.

BTW, I'm not sure what "pre post" means in the title of this PR.

I didn't comment on notation, as that is being discussed in #2271.

I'm hoping that @Alizter will have time to take a look, maybe after my feedback has been addressed.

theories/Basics/PathGroupoids.v

theories/WildCat/TwoOneCat.v

jdchristensen · 2025-04-28T13:05:42Z

theories/WildCat/TwoOneCat.v

+    (p : f $=> f') (p' : g $=> g'),
+    (p' $@R f) $| (g' $@L p) $== (g $@L p) $| (p' $@R f');


It would have been better to make the change to the notation in a separate commit, as the diff is now harder to read.

theories/WildCat/TwoOneCat.v

jdchristensen · 2025-04-28T13:23:08Z

theories/WildCat/TwoOneCat.v

+  rapply is0bifunctor_flip.
+Defined.
+
+Notation "alpha $@@ beta" := (fmap11 cat_comp beta alpha) : twocat.


Now there are two meanings for $@@. Is the plan to unify them?

It makes sense to unify them. I'll take another look at this PR and figure out whether it's appropriate for the current PR or would require extensive refactoring.

theories/WildCat/Universe.v

jdchristensen · 2025-04-28T13:32:28Z

theories/WildCat/Paths.v

+  - exact (@concat_pV A _ _ _).
+  - exact (@concat_Vp A _ _ _).


apply concat_pV. and apply concat_Vp. work and are cleaner.

theories/WildCat/Paths.v

jdchristensen · 2025-04-28T13:42:14Z

theories/WildCat/Core.v

+Class AreInverse {A} `{Is1Cat A} {a b : A} (f : a $-> b) (g : b $-> a) :=
+  {
+    inv_issect : g $o f $== Id a;
+    inv_isretr : f $o g $== Id b;
+  }.


We also have Cat_IsBiInv which uses bi-invertibility. Maybe it makes sense to have these separate, but it's worth thinking about.

patrick-nicodemus · 2025-04-29T22:37:12Z

Sorry, the name was just a lazy way of distinguishing it from the previous PR. In this PR, the definition of IsBicat takes pre- and post-whiskering of a 2-cell with a 1-cell as primitive, as opposed to a binary horizontal composition operation for 2-cells.

patrick-nicodemus · 2025-05-20T16:23:34Z

Addressed some comments but not all, I will come back to address these

jdchristensen

This is looking good. I especially like the new comments which make it much easier to understand what you are doing. As you mention, there are a couple more comments to respond to. And I think it would be a good time for @Alizter to take a look at this PR if he is able to.

jdchristensen · 2025-05-21T17:53:02Z

theories/Pointed/Core.v

+  - intros ? ? ? ? f g h; exact ((pmap_compose_assoc h g f)^* ).
+  - intros ? ? f; exact (pmap_postcompose_idmap f).
+  - intros ? ? f; exact ((pmap_postcompose_idmap f)^* ).
+  - intros ? ? f; exact (pmap_precompose_idmap f).
+  - intros ? ? f; exact ((pmap_precompose_idmap f)^* ).


In the lines with ^*, you can remove the outer parentheses.

jdchristensen · 2025-05-21T17:53:35Z

theories/Pointed/Core.v

-    1: reflexivity.
-    by pelim f g.
+  - intros A B C D; snapply Build_Is1Natural.
+    (* TODO: It would be nice if this naturality proof could reuse the proof in the


No line break in comment.

jdchristensen · 2025-05-21T17:54:55Z

theories/WildCat/Paths.v

+  - intros a b f. exact ((@concat_p1 A _ _ f)^).
+  - exact (@concat_1p A).
+  - intros a b f. exact ((@concat_1p A _ _ f)^).


In the two lines with ^, you can remove the outer parentheses.

patrick-nicodemus marked this pull request as ready for review April 1, 2025 16:59

patrick-nicodemus force-pushed the bicategory_pre_post branch from 4d18146 to 46398a1 Compare April 9, 2025 13:47

jdchristensen reviewed Apr 28, 2025

View reviewed changes

patrick-nicodemus changed the title ~~Bicategory pre post~~ Bicategory (Is1Cat compatible design) Apr 29, 2025

Patrick Nicodemus added 5 commits May 20, 2025 11:58

Defined bicategory, refactored (2,1)-cat onto bicat.

9165dc1

Refactor some 1Cats as bicats w invertible 2-cells

961884c

Refactored 1Gpd to use AreInverse

e3add99

Convert a 1-category to a 1-bicategory.

9a3e60c

undid change to master

ee99c2c

patrick-nicodemus force-pushed the bicategory_pre_post branch from 46398a1 to 80de9be Compare May 20, 2025 16:18

Some changes in response to reviewer comments

a37ad55

patrick-nicodemus force-pushed the bicategory_pre_post branch from 80de9be to a37ad55 Compare May 20, 2025 16:22

jdchristensen reviewed May 21, 2025

View reviewed changes

		(p : f $=> f') (p' : g $=> g'),
		(p' $@R f) $\| (g' $@L p) $== (g $@L p) $\| (p' $@R f');

Bicategory (Is1Cat compatible design) #2272

Are you sure you want to change the base?

Bicategory (Is1Cat compatible design) #2272

Uh oh!

Conversation

patrick-nicodemus commented Apr 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jdchristensen commented Apr 27, 2025

Uh oh!

Alizter commented Apr 27, 2025

Uh oh!

jdchristensen left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

patrick-nicodemus commented Apr 29, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

patrick-nicodemus commented May 20, 2025

Uh oh!

jdchristensen left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

patrick-nicodemus commented Apr 1, 2025 •

edited

Loading

patrick-nicodemus commented Apr 29, 2025 •

edited

Loading