monads are lax functors

[4e554c4c]

I noticed this on the nlab and it sounded fun to write down.
Really it'd be nice to do this using displayed bicategories with a displayed bicategory of monads over a base bicategory $$\mathsf{S}$$.

Description

• A few facts about the terminal category
• The terminal bicategory
• Monads are equivalent to lax functors from said bicategory

Checklist

Before submitting a merge request, please check the items below:

• I've read the contributing guidelines.
• The imports of new modules have been sorted with support/sort-imports.hs (or nix run --experimental-features nix-command -f . sort-imports).
• All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content, and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title with chore:.

[Lavenza]

Pull request preview

New pages

• Cat.Bi.Instances.Terminal (+35, -0)
• Cat.Instances.Shape.Terminal.Properties (+29, -0)

Changed pages

• Cat.Bi.Diagram.Monad (+68, -5)
• Cat.Bi.Base (+7, -5)
• Cat.Instances.Shape.Terminal (+3, -0)
• Cat.Functor.Naturality (+0, -1)

[4e554c4c]

a quick note: to say that monads are lax functors (i.e. with a path) we would need some kind of Monad-path and lax-functor-path lemmas... which don't really seem to be possible with the current state of tri-category theory in 1lab.
happy to add them tho lol

[ncfavier]

to say that monads are lax functors (i.e. with a path) we would need some kind of Monad-path and lax-functor-path lemmas... which don't really seem to be possible with the current state of tri-category theory in 1lab

Do we need any of that? The automatically generated path lemmas that don't build in any univalence should be enough since all the relevant structure seems to be mapped strictly?

[4e554c4c]

should be fixed now. it's kind of hard without the workflow giving a preview sorry