Ralph Matthes

By the way, Mark has a position in Toulouse.

I have the bad feeling that in our situation, colimits are not preserved, and so, we should not go for creation of colimits in the sense of displayed categories (that...

Commit [7fe3c26d5](https://github.com/UniMath/UniMath/pull/1384/commits/7fe3c26d5a6f1) is separated out into a new PR #1387 and the present PR will be paused for further insights from category theory.

The heading should then be changed a bit. Any publication that comes with a contribution to UniMath also serves as documentation of (that part of) UniMath. But also a publication...

How about one unordered list, but a letter indication for the three categories: G for global, L for local, E for external use (and multiple letters could be warranted for...

I was ready to add the following to that page: Categories of papers listed here We try to indicate the category to which a listed article belongs. There are *...

I have integrated the extra contents of the obsolete page into the current one before deletion. In general, there could be more links to the preprints. Obviously, some papers are...

If this was the path to follow, I would even more need to separate `SubstitutionSystems` into the main part that that does not depend on `Bicategories` and the small fraction...

There were very few shortcuts in that move in the sense that I did not redo something for `z_iso` but instead used the equivalence with `iso`. So, we are not...

It took me a very long time to come back to this question. Thanks a lot @DanGrayson . If I replace `hnf` in your proposal by `cbv [pr1 pr2]`, I...