IC for some higher category theory

[4e554c4c]

i wanted to check on weather some general higher category structures would be desired in the 1lab

i was thinking about working on lax/pseudomonads or doctrines, but currently the tricategory theory in the 1lab isn't developed to the point that this would be possible.

also working out 2-topoi could be cool

lmk what y'all think

[TOTBWF]

That would be very much appreciated! In general, fleshing out bicategory theory would be very nice. I'd suggest looking at the series of papers on displayed bicategories; there's a lot of good design insights to glean.

[4e554c4c]

yeah i was looking at this recently (and discussed with @ncfavier on IRC). the displayed bicategory of monads seems like a good start