tillrampe
tillrampe
I can still split it up. Wouldn't take long.
Thanks for the feedback. What I will do is the following. I'll split up the pull request into - coequalizer (improvements on the existing library) - local coequalizers (improvements on...
As of now, this pull request type-checks, but it will need revision. Among the things to improve are: - Don't `import` in `where`-clauses. - Use `using`-commands wherever feasible. - Don't...
I am considering changing the directional indicators `ˡ` and `ʳ` as in `actionʳ` and `actionˡ` from diagrammatic order to algebraic order. Algebraic order seems to be the common choice in...
There is still a lot more to change, but at least the variable names in `TensorproductOfBimodules` and `TensorproductOfHomomorphisms` are improved. They are hopefully clearer now, and many of them are...
I will be rather busy until beginning of October. So, I might not be able to make changes to this pull request. I will finish this, however, as soon as...
Don't think so. I've mainly executed the changes we agreed were necessary before; like using `push`, `pull`, etc. from `Morphism.Reasoning` to shorten proofs, and not `renaming` fields of `Bimodule` and...
This is ready for re-review now. It all type checks on my device.