Some stuff im working on

[4e554c4c]

hi, thought i'd write this down since I don't want to step on anybody's toes or duplicate work.

I have a few things that I'm working on that I'd like to PR in the next few months (checked off means I PR'd it lol).

Primarily:

• Total categories (where there is an adjunction ($れ \dashv よ$)
  • There are a few alternative names for the adjoint. We also could do $さ$ as in 左(さ)辺(へん) .
  • An explicit description of free objects with respect to よ (as colimits)
    • I need some help figuring out a name for these. This mathoverflow post raises the question and "corepresentation" is posed... but this has a different meaning in the 1lab. We could go with Shulman's "realization" or w/e.
  • A special adjoint functor theorem for total cats (every cocontinuous functor has a right adjoint)
  • Proof that topoi are co/total.
• The bicategory of $T$-Spans over a cartesian monad.
  • The definition of a cartesian monad and some examples/prose.
    Maybe we should use a different name so not everything is named after dat guy.
  • ? I could refactor ordinary spans to be $1$-Spans, but I think this would go against the theme of simple definitions in the 1lab.

[TOTBWF]

Realisation seems fine for the free objects. Not sure how I feel about れ or さ though; seems like it could make things difficult to read.

As for T-spans, be warned. I've tried this before in the past and it's extremely brutal. This is probably best done at the level of double categories instead of bicategories. If you have a strong stomach you could also try for S-T-spans for a pair of cartesian monads equipped with a cartesian distributivity law; the algebra will only be marginally worse.

[4e554c4c]

As for T-spans, be warned. I've tried this before in the past and it's extremely brutal. This is probably best done at the level of double categories instead of bicategories.

i definitely want to look at double categories of spans, but maybe later.
i do have almost everything for T-spans done already "only" missing the triangle and pentagon identity so this seems relatively doable (see here for code and diagrams but not very much prose)