Double Category Theory from a Double Categorical Perspective


This is a companion discussion topic for the original entry at https://forest.localcharts.org/topos-0005.xml

It was an interesting experience trying to take live notes in forester collaboratively.

Ultimately, I think the experiment was a failure; we decided to not do this in the future.

Partly this is because there are so many diagrams in category theory, and quiver can’t quite keep up.

Partly, this is because VSCode LiveShare is not a correct implementation of collaborative editing; people ended up being kicked out randomly, and I noticed that occasionally after many people were editing the same file, what was shown on screen and what existed on disk would diverge, even after I closed and reopened the file. I had to diagnose using cat the difference between the two, and then delete and rewrite the entire line.

Partly, this is because forester is hard to use for new users. There are many design decisions which I ultimately agree with (like using \ul{\li{...}\li{...}} for lists, or making every paragraph be in a \p{}), that nevertheless make it hard for people to get started. It really does exist in a no-man’s land between latex and HTML, to the extent that it only makes sense if you are familiar with both.

This is compounded by the fact that because forester is based on balancing braces, one unbalanced brace can break the entire build, and it can be hard to diagnose where that is. In a more “local” format like markdown, a user editing a different paragraph can’t break my paragraph. Of course, the ability to make multiple trees helps with this to a certain extent. But it’s still something to think about. HTML/XML, with its matching closing tags, actually has more of an ability to gracefully handle this kind of failure.

It would be still helpful if errors could be more localized, so that certain portions of the document showed up as an error, but the remainder of the document still compiled.

But ultimately, it may just be the case that producing high-quality notes live is very hard. I was hoping that working collaboratively might solve some of these problems, as one person can focus on making quiver documents, another person can focus on top-level structure, etc., but we didn’t really seem to “get off the ground”, and people seemed to eventually give up on forester.

1 Like

What I don’t understand about Forest (and what is keeping me from just go ahead and write everything there) is the syntax… why a new one? Why not Markdown or LaTeX or a reasonable hybrid like the nLab?

It is kind of “a reasonable hybrid” of LaTeX and HTML, and a smidgeon of markdown for the links like [title](url). But almost everything is with \, just like LaTeX; it is a very uniform syntax.

To answer specifically:

  • Why not “just markdown” – markdown is not extensible. Stuff like queries would still need a new syntax, and then we’d have to figure out what that is. Also, markdown is actually incredibly janky. See the rationale for djot, another new format written by the author of pandoc, which includes gems like
  1. Rules for emphasis should be simpler. The fact that doubled characters are used for strong emphasis in commonmark leads to many potential ambiguities, which are resolved by a daunting list of 17 rules. It is hard to form a good mental model of these rules. Most of the time they interpret things the way a human would most naturally interpret them—but not always.
  • Why not “just latex” – there are n+1 tools which claim to compile LaTeX to HTML, and all of them work 95% of the time, and absolutely screw up the rest. Also, they are usually frankenstein hybrids of Perl+whatever LaTeX is written in+Python+… Forester going their own way and not depending on running a TeX compiler means that large forests can still be compiled in <1sec.

Choosing to have a uniform, TeX-inspired syntax with everything being \command leads to a consistent experience, and given that we don’t want to relearn how to write math so \stuff is going to be inside of our equations, it makes sense to just make the whole syntax that to be consistent. This also is the only way that we can have macros which work

  • in the main body of the text
  • in equations
  • in parts of the document (like commutative diagrams) which are compiled via LaTeX and then included as SVGs.

So while I agree with you that empirically it’s quite daunting for new users to get used to something unfamiliar, I think that there is a reason why almost every tool which has tried to go your route (use markdown or LaTeX or a “reasonable hybrid”) has ended up with a ton of confusing corner cases, and has ended up not extensible.

But I think there is still a lot of room for improvement in forester: fortunately Jon Sterling seems very responsive to new ideas, so hopefully we can continue sanding down the edges as it were.

1 Like

You give good arguments for why Forest has a superior syntax from a technical standpoint (aside: reading the djot rationale is hilarious—as a user, I care very little how easy it is to build a parser for it). And this does eventually improve UX, I guess. But it’s frustrating to be trapped in xkcd 927 when it comes to knowledge sharing. Every time someone comes up with a new platform, format, syntax, whatever with very little interoperability and this means we are missing big compounding effects. It seems there’s very little effort in trying to be somewhat interoperable or at least lean on existing syntaxes (e.g. I don’t think anything Forest does couldn’t be done via HTML or possibly HTML-friendly XML). That also guarantees portability and longevity by the way.

I’m shaking my fists at the clouds, I know. If I had to start mathblogging/note taking from scratch, I’d probably start with Forest too. But it’s so tiring to keep changing platforms…

Here’s a question: what if there were a markdown → forester converter that made it easy to migrate things into forester? Would that make a material difference?

Also, part of the reason why we aren’t standardized is that everyone and their dog has their own markdown+latex hybrid which makes slightly different design decisions, and so are incompatible, and also none of them are extensible. The forester syntax, which is far easier to parse than markdown, and is intrinsically extensible, would be a much better candidate for an ecosystem sharing one format.

If you want to make something better than other things, you will have to crack some compatibility eggs.

See Quarto for an example of trying to retain compatibility and as a consequence being slow, bloated, and incorrect.

Edit: sorry if I’m being overly combative here, and digging in after you said that you substantially agree with me. I want to say that I also very much appreciate how you care enough about this to argue about it, because it means that there’s some chance that you would use something in an adjacent space, which means that I do care very much about whether it’s a smooth experience for you. So perhaps just concentrate on the first thing I said in this post rather than the rest, which it looks like you did!

1 Like

It’d help a bit to have something like a \markdown macro I can lazily write Markdown into. Still, Forest makes really peculiar, if well-motivated, design decisions around the notes organization which really intrigue me but also add quite a bit friction.

Perhaps the best thing to promote adoption is to have a short tutorial where you explain the main concepts of Forest and how to start writing on it. You can skip the installation part and direct it to LocalCharts users.

Yes, I think that writing a tutorial is a very good idea! And I hope that we can figure out how to remove that friction through stuff like IDE support, macros, etc.

1 Like

I think that in an ideal world, we could make a “visual editor” for forester, which presented something like a WYSIWIG interface while editing the text files, similar to Overleaf’s visual editor for LaTeX. And then ideally this would be collaborative. But one step at a time…

1 Like