Standardize arrow styles in diagrams

[florian-rabe]

We have the following kinds of theory morphisms

• meta (in some sense, a special case of include)
• include (in some sense, a special case of structure)
• structure
• view

It would be good to have a standard way of styling these, i.e., to assign

• arrow tips (e.g., hooked for include)
• arrow line style (e.g., double for view)
• arrow color

We might want to make color optional so that

• it does not interfere with b/w printing
• color can be used for orthogonal styling in UIs

@kohlhase @jbetzend @tkw1536 @Jazzpirate

[florian-rabe]

So far, I've tried to use only hooked and double. I never used anything special for structures.

Also note that structures and view are usually labeled with their names.

[kohlhase]

I have already done that for tikz pictures in https://github.com/KWARC/localmh/blob/master/sty/pgflibrarytikzmmt.code.tex to use it just use

\usetikzlibrary{mmt}
\begin{tikzpicture}
\node[thy] (a) at (0,0) {foo};
\node[thy] (b) at (0,1) {bar};
\draw[include] (a) -- (b);
\draw[view] (a) --  (b); 
\draw[struct] (a) -- (b);
\end{tikzpicture}

This has helped consistency in my papers very much. This conforms to my current taste in arrows: single straight arrows for structures single squigly arrows for views hooked arrows (there are left and right version) for includes dotted arrows for meta.

[kohlhase]

There are also other useful things like pushout annotations, ....

[kohlhase]

But I guess that with standardize, you mean standardize everywhere (i.e. also in TGView, ... ) I am all for that.

[lambdaTotoro]

Just for the record: Should we ever chose to make colours carry meaning in the theory graphs ( and not just in e.g. the logo, see issue #174 ), we should take care to chose a colour palette that doesn't make it harder for colourblind people to read the information conveyed, like e.g. red/green would.

[kohlhase]

I am completely against using color for semantics in TG.

[lambdaTotoro]

I can see why, I wouldn't want that, either. If this isn't actually considered, disregard above comment.