Bicategory (Is1Cat compatible design)#2272

Open

patrick-nicodemus wants to merge 6 commits intoHoTT:masterfrom

patrick-nicodemus:bicategory_pre_post

Commits on May 20, 2025

Defined bicategory, refactored (2,1)-cat onto bicat.
Patrick Nicodemus
committed
Refactor some 1Cats as bicats w invertible 2-cells
Patrick Nicodemus
committed
Refactored 1Gpd to use AreInverse
Patrick Nicodemus
committed
Convert a 1-category to a 1-bicategory.
Patrick Nicodemus
committed
undid change to master
Patrick Nicodemus
committed
Some changes in response to reviewer comments
Patrick Nicodemus
committed