Michael Lindgren

Also I just noticed that you made this PR from your `master` branch of your UniMath fork. As a general recommendation it is better to work in topic branches instead...

@benediktahrens no this is still a WIP, It needs some work and testing. I'm trying to figure out some permission issues currently.

I think we should be very careful about merging this. This will effectively enable `-type-in-type` in **every** project that use UniMath, without them knowing it. It is my opinion that...

There are probably optimizations to be done in the dependency graph that would involve not only removing unnecessary imports but also splitting some files into smaller ones, which would in...

I always forget where `show_id_type` is defined and have to look for it. I would love to have it defined somewhere in Foundations (maybe easier to write on a post-it...

I put some more thought into this. Minimizing imports using a script that only work on individual files, and test whether or not the file compiles with a certain import...

Is it a problem having two different implementations in the library? (besides the fact that the displayed one seems to cause compilation issues currently) Or are they not different enough...

So this is probably not related to the issue at hand, but this confuses me: Shouldn't the displayed implementation of full subcategories take a `P : hsubtype C` instead of...

I like this idea. I would also be in favor of moving the definitions of `po` (we should give this a more descriptive name IMO), `Poset` etc, and their associated...

Related: #1067.