Ralph Matthes

Should be fine again.

@nmvdw Thanks a lot for this valuable feedback. It is a bit unfortunate that dialgebras have their characteristic equality oriented differently from the comma category of which they are a...

@nmvdw I am sorry for my bad use of English grammar: I had intended to say that the equality for dialgebras is a special case of the one for comma...

@benediktahrens This PR has grown from a better connection within the UniMath library to (hopefully) new research. I might have identified the inserter in the bicategory of monoidal categories, but...

I do not intend to contribute more material to this PR, another one is in preparation. So, please merge if it seems sound.

I would like to remind you of missing type information in some definitions in PartA.v that were part of my previous PR #764. There are two types of suggestions: add...

@DanGrayson : if you drop `mkpair`, then please also remove `mk_pair` in [UniMath/CategoryTheory/limits/pullbacks.v](https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/limits/pullbacks.v#L546) which can equally be replaced by `use tpair` at the only place where it is used.

It succeeded but the intended simplifications mostly failed - this is only seen in the Coq comments.

@DanGrayson : I thank you for your comment, but I do not see how to use the Fail command in my situation. I would ask to interpret as failure if...

The code that fails to do what I want is at line 157. How could that comment be turned into an explicit failure? I have to see why the build...