do something about alternative definitions.
Sometimes we have alternative definitions, where the (semantically) same object is defined in two ways. A well-known instance is groups defined via multiplicative operation (unitary with inverses) or via a division operator (cancellative quasigroups). Another example is the Cahen constant.
We currently make separate definitions for those and then establish a biview between them. But we need to have "alignment-type" annotations that are more lightweight, and can be picked up in the glossary. E.g. by displaying all definitions for a given concept instead of having the lemma twice. Same holds for the generated dictionary.
I am thinking about something like new keys eqdef
, eqrepos
, eqtoview
, eqtoviewrepos
, eqfromview
, and eqfromviewrepos
for \begin{modsig}
. E.g.
\begin{modsig}[eqdef=foo,eqrepos=smglom/calculus,
eqtoview=foo2bar,eqfromrepos=smglom/calculus,
eqfromview=bar2from]{bar}
This defines an alternative definition module bar
for foo
, which is in smglom/calculus
and justifies this by two views foo2bar
and bar2foo
, which (here) go from module bar
to foo
and back.
We should probably allow the back view to go to another module foobar
, which is an alternative definition for foo
, so that the overall view structure is a full cycle. This is a figure we see in maths quite often, something like
The following three definitions for ``baz`` are equivalent
- foo
- bar
- foobar
proof
- foo -> bar
- bar -> foobar
- foobar -> boo
That should be supported.