Author: Urs Format: MarkdownItexclearing this ancient, abandoned and redundant entry,
following the discussion [here](https://nforum.ncatlab.org/discussion/14319/community-history/?Focus=99016#Comment_99016).
<a href="https://ncatlab.org/nlab/revision/diff/Notation+%3E+history/15">diff</a>, <a href="https://ncatlab.org/nlab/revision/Notation+%3E+history/15">v15</a>, <a href="https://ncatlab.org/nlab/show/Notation+%3E+history">current</a>
clearing this ancient, abandoned and redundant entry,
following the discussion here.