Benedikt Ahrens

@Alizter : Thanks a lot for your message. UniMath is currently working with `-noinit`. The issue has morphed to be about `Init.Logic` now. I'll change the title of the issue...

On 12/11/2018 14:04, Daniel R. Grayson wrote: > If we got rid of |precategoryWithBinOps|, we could probably also get rid > of this silly rewriting rule: > > |Lemma rewrite_op...

On 12/06/2017 02:40 AM, Langston Barrett wrote: > @benediktahrens Thanks for taking a > look! Do you have feedback on whether I should rephrase |islinv|, > |isrinv|, |isrinvertible|, etc. in...

The PR does not currently compile, see, e.g., https://travis-ci.org/UniMath/UniMath/jobs/312201293 . Could you fix these errors, please?

On 12/07/2017 08:18 PM, Langston Barrett wrote: > @benediktahrens Actually, I just realized that making `hasinv` into a > sigma-type makes this whole construction fail. Then we can't define >...

I think I understand better now what the issue is. I hadn't looked at the code properly. There is the following definition: ``` Definition invertible_elements : hsubtype X := fun...

@siddharthist : could you update this PR, please? There is currently a merge conflict in CT/.package/files. I suggest we merge this PR and you think about naming conventions afterwards.

``` COQC UniMath/CategoryTheory/Actions.v File "./UniMath/CategoryTheory/Actions.v", line 230, characters 55-58: Error: The reference rng was not found in the current environment. Command exited with non-zero status 1 0.39user 0.09system 0:00.49elapsed 99%CPU...

@DanGrayson : you had asked for changes here. Have they been addressed?

See https://travis-ci.org/UniMath/UniMath/jobs/456369958#L1661 for one compilation failure. It has to do with the addition of the symmetric associativity law to categories, I assume. ``` File "./UniMath/CategoryTheory/Categories.v", line 213, characters 12-40: Error:...