Ralph Matthes

I have started attacking this problem.

The outcome of the UniMath 2019 school on Rech's construction is [ComputationalM.v](https://github.com/UniMath/UniMath/blob/master/UniMath/Induction/M/ComputationalM.v). The extension to families was under way. Rech had this already before, but his code was not connected...

I assume this is because both conclusions are logically equivalent, and `is_z_isomorphism f` is also a proposition when C is a category, and univalence is only studied for categories. We...

This starts looking like a project to dismiss the current definition of `iso` (after getting all files compile again). Are there more global considerations that stand against this move? Maybe...

I would like to attract attention to [my commit](https://github.com/UniMath/UniMath/commit/a8ce0401) that would need help from an expert in displayed categories - just to fix proof parts of a definition where the...

A great help indeed. Thanks a lot @nmvdw .

Please see my PR #1507. It asks for more help on seven identified files - among the 153 .v files that were adapted so that all ~650 files of UniMath...

It is rather a request for comments. No conflict with #1391 envisaged. The main question: is it good to have two separate strands instead of first developing the stuff without...

Good explanation. I cannot decide on that matter. Is the code copying acceptable in the present form - hence with rather long file names? Would more of the developments involving...

I am trying to resolve the conflicts still today.