This tool is fantastic! I was able to generate a Fourier-Poisson cube [0] in about 10 minutes, and the UI is incredibly intuitive.
The focus on commutative diagrams, rather than a free-form canvas, is a brilliant design choice that keeps it clean and easy to use. I wish I'd had this during my thesis; it would have saved so much time.
Petri nets are cool. They’re sort of like if finite state machines could be multithreaded.
I first found out about petri nets when reading the writings of an organization called “statebox”. Statebox was interested in petri nets and commutative diagrams (as well as many other category theory concepts). I read some of their papers, was entranced, and it became my dream to work there. Unfortunately their homepage now is just the text “imagine being a category theorist” with a laughing-crying emoji, so I have no idea what happened to them.
Just used this a few days ago to draw a simple diagram [0] for my book [1]!
Unfortunately, because it is for category theory only, it doesn't have much support for prettifying your nodes, but you can do that with the latex, of course.
I was using https://tikzcd.yichuanshen.de/ last night, which is basically a less feature-filled version of this. It’s quite nice for doing simple diagrams, though.
They're just a nice way of writing equations between functions (or other things that compose like functions).
This is a picture of a function f that takes inputs from A and produces outputs in B
f
A → B
and this diagram
f
A → B
↘ ↓ g
h C
just means g ∘ f = h, ie. doing f then g is the same as doing h. Since you write the domain and codomain of each function, it makes it easier to see when the functions can compose (ie. when it type checks).
Because paths through a diagram themselves compose like functions do, this notation turns out to be very natural. For example, associativity is inherent in the notation: A→B→C→D is the only way to express the composition of three functions, you can't even write the difference between (f∘g)∘h and f∘(g∘h).
A commutative diagram is just a collection of nodes and directed edges between nodes (aka, a directed graph), but it's a directed graph along with the claim that any two paths in this graph which start at the same node and end at the same node are to be considered equivalent, in some sense.
In general, a directed (multi)graph along with an account of which of its paths are and are not to be considered equivalent to each other (where this equivalence relation satisfies some basic nice properties) is known as a "category". This concept comes up ubiquitously in math/abstract logic/etc. Commutative diagrams are useful for quickly visually reasoning about equivalences of paths in such contexts.
Each capital letter is a type and each lower case letter is a function from one type to another. You can trace a path in the diagram to talk about a bunch of function calls (e.g following f then g then n represents n(g(f(a)))). This is called a diagram. Then the statement that a diagram is commutative says that if you trace any two paths that share a start and end, they are equal.
So n(g(f(•))), s(r(l(•))), s(m(f(•))) are all paths/function calls you could make to get from A to C'. Since the diagram is said to be commutative, those paths are all equal.
Being a monomoprishm, epimorphism, or isomorphism are all important properties of functions that say you're allowed to "cancel" on both sides of an equality. e.g. in general, if f(g(x))=f(h(x)), you can't conclude that g(x)=h(x). If f can be cancelled in that way, it's called a monomorphism. Similarly if g(f(x))=h(f(x)) lets you cancel the f to get g(x)=h(x), f is called an epimorphism. An isomorphism is both. This kind of thing let's you "walk backwards" along some paths in the diagram in certain situations.
One flavor of theorem you might see in category theory (like the example five lemma[0]) looks like "look at this diagram. if g is an epimorphism and h is a monomorphism then f is an isomorphism". So if I know I can cancel this way and that way, I learn I can cancel this other way.
> The five lemma states that, if the rows are exact, m and p are isomorphisms, l is an epimorphism, and q is a monomorphism, then n is also an isomorphism.
Its a way of demonstrating that two paths through a diagram are in some sense equal. The dots in the corners are objects and the arrows are morphisms.
To keep this simple just imagine the objects are types and the arrows are functions between those types.
You start out in the upper left corner and walk through the two paths checking the types as you go along. If the diagram typechecks correctly then it is said to commute and the two paths are in some sense equivalent. The specific sense depends on a bunch of details elided here.
It would help if you read the definition of a category. It is very abstract but also pretty simple with just a couple of axioms.
An example of a category is the "sets and functions" category. In that category, every conceivable set lives as an object (node) and every conceivable function between any two sets lives as an arrow between these two sets.
So, you can take an arrow from A to B and one from B to C and compose them like you would do with functions to get a function from A to C.
A commutative diagram would then be a subset of the whole category, where following all depicted paths between two sets X and Y would yield the same function if for each path you composed all the arrows belonging to it.
I haven't read anything on higher categories so I am not sure about pasting diagrams, but they are probably something along these lines, generalized in some way.
Wikipedia pages for niche STEM topics tend to be made by 1 or 2 people, obsessed with the topic, but often not very good at high level abstract communication. So you get a technically-correct mess like that article. If you are an expert in a niche stem topic, look up the wikipedia article for it, then use that experience to fight the Gell-Mann Amnesia effect for the rest. I use wikipedia for a lot of topics, but not topics like this. An LLM is a better bet these days.
Is there a possibility to export in a web-friendly format? I guess SVG would be it? If I ran quiver in localhost then sharing via a link is not an option.
Quiver was absolutely indispensable when I did a category theory course a few years ago. The UI was clean, intuitive, and featureful. Compared to banging one's head against Tikz, it's absolutely no contest.
Very nice product! In the past I usually wrote TikZ code by hand and it was pretty fast but now I forgot a lot of that stuff and this could be very useful for commutative diagrams.
rhymer|1 year ago
The focus on commutative diagrams, rather than a free-form canvas, is a brilliant design choice that keeps it clean and easy to use. I wish I'd had this during my thesis; it would have saved so much time.
[0] https://q.uiver.app/#q=WzAsOCxbMCwxLCJnIFxcdGV4dHsgb24gfVxcb...
atkirtland|1 year ago
ChadNauseam|1 year ago
Petri nets are cool. They’re sort of like if finite state machines could be multithreaded.
I first found out about petri nets when reading the writings of an organization called “statebox”. Statebox was interested in petri nets and commutative diagrams (as well as many other category theory concepts). I read some of their papers, was entranced, and it became my dream to work there. Unfortunately their homepage now is just the text “imagine being a category theorist” with a laughing-crying emoji, so I have no idea what happened to them.
ljouhet|1 year ago
practal|1 year ago
[0] https://q.uiver.app/#q=WzAsNSxbMSw2LCJcXHRleHR7TmF0dXJhbCBEZ...
[1] http://abstractionlogic.com
xanderlewis|1 year ago
sebmellen|1 year ago
The Wikipedia page was too abstract for me to understand at a basic level [0].
[0]: https://en.wikipedia.org/wiki/Commutative_diagram
edflsafoiewq|1 year ago
This is a picture of a function f that takes inputs from A and produces outputs in B
and this diagram just means g ∘ f = h, ie. doing f then g is the same as doing h. Since you write the domain and codomain of each function, it makes it easier to see when the functions can compose (ie. when it type checks).Because paths through a diagram themselves compose like functions do, this notation turns out to be very natural. For example, associativity is inherent in the notation: A→B→C→D is the only way to express the composition of three functions, you can't even write the difference between (f∘g)∘h and f∘(g∘h).
Chinjut|1 year ago
In general, a directed (multi)graph along with an account of which of its paths are and are not to be considered equivalent to each other (where this equivalence relation satisfies some basic nice properties) is known as a "category". This concept comes up ubiquitously in math/abstract logic/etc. Commutative diagrams are useful for quickly visually reasoning about equivalences of paths in such contexts.
ndriscoll|1 year ago
So n(g(f(•))), s(r(l(•))), s(m(f(•))) are all paths/function calls you could make to get from A to C'. Since the diagram is said to be commutative, those paths are all equal.
Being a monomoprishm, epimorphism, or isomorphism are all important properties of functions that say you're allowed to "cancel" on both sides of an equality. e.g. in general, if f(g(x))=f(h(x)), you can't conclude that g(x)=h(x). If f can be cancelled in that way, it's called a monomorphism. Similarly if g(f(x))=h(f(x)) lets you cancel the f to get g(x)=h(x), f is called an epimorphism. An isomorphism is both. This kind of thing let's you "walk backwards" along some paths in the diagram in certain situations.
One flavor of theorem you might see in category theory (like the example five lemma[0]) looks like "look at this diagram. if g is an epimorphism and h is a monomorphism then f is an isomorphism". So if I know I can cancel this way and that way, I learn I can cancel this other way.
[0] https://en.wikipedia.org/wiki/Five_lemma
> The five lemma states that, if the rows are exact, m and p are isomorphisms, l is an epimorphism, and q is a monomorphism, then n is also an isomorphism.
solomonb|1 year ago
To keep this simple just imagine the objects are types and the arrows are functions between those types.
You start out in the upper left corner and walk through the two paths checking the types as you go along. If the diagram typechecks correctly then it is said to commute and the two paths are in some sense equivalent. The specific sense depends on a bunch of details elided here.
d_tr|1 year ago
An example of a category is the "sets and functions" category. In that category, every conceivable set lives as an object (node) and every conceivable function between any two sets lives as an arrow between these two sets.
So, you can take an arrow from A to B and one from B to C and compose them like you would do with functions to get a function from A to C.
A commutative diagram would then be a subset of the whole category, where following all depicted paths between two sets X and Y would yield the same function if for each path you composed all the arrows belonging to it.
I haven't read anything on higher categories so I am not sure about pasting diagrams, but they are probably something along these lines, generalized in some way.
unknown|1 year ago
[deleted]
geor9e|1 year ago
unknown|1 year ago
[deleted]
atheiste|1 year ago
3PS|1 year ago
vouaobrasil|1 year ago
pizza|1 year ago
dccsillag|1 year ago
sundarurfriend|1 year ago
instakill|1 year ago