Benedikt Ahrens

@DanGrayson : could we work on updating the Coq submodule? It will require some changes to `Makefile`, in particular, the `CONFIGURE_OPTIONS` need to be adapted.

Done in #1541 , closing.

On 18/12/2018 02:12, Daniel R. Grayson wrote: > These notations > > |Module Export Notation. Notation ap := maponpaths. Notation "p # x" := > (transportf _ p x) (right...

In particular, @DanGrayson suggested aligning the level of composition with that of multiplication.

What is the status of this PR? Is the goal to have it merged? Or is it only a basis for discussion? Also, will it be in conflict with #1391...

There are two orthogonal, but intersecting, questions: 1. What is the right notion of category? 2. Should one formalize stuff in terms of displayed machinery? The answer to 1 is...

The Coq Platform 2021.09 has been released now: https://github.com/coq/platform/releases/tag/2021.09.0. It features a reasonably recent version of UniMath, which is good enough for the material of the UniMath schools, for instance:...

Is this PR ready for review/merging?

The PR contains a construction for not-necessarily univalent categories that already exists for univalent categories. Why are we interested in the construction on non-univalent categories?

File PartD could look much better if (unicode) notation were used throughout, e.g., instead of `weq`. Is there a chance we can fix this before December?