Niels van der Weide

It is not that important of a change and, if it is not universally accepted, then it is necessary to do.

> Why not add `#[local] Unset Universe Checking` just to the minimal set of files that need it? (Just run `make` and add the setting to whatever files fail, and...

I try to minimize imports except for Foundations/MoreFoundations, because to me, it is not always obvious which files in those directories are actually needed. I don't think that the benefits...

> I have the impression that my switch from the former to the latter implementation in the Eilenberg-Moore category now leads to unbearably slow compilation of PR #1768. This occurs...

We could implement full subcategories in the following ways: 1. The input is a category `C` and a predicate `P : C -> hProp` (i.e. `hsubtype C`) 2. The input...

This issue is also related to: https://github.com/UniMath/UniMath/blob/master/UniMath/Bicategories/DaggerCategories/BicatOfDaggerCats.v#L73. I think this coercion should be removed, because when playing around with coercions on bicategories, I noticed they didn't behave well.

@rmatthes This issue is solved, right?

> For me, this proposal implies that the work leading to Pataraia's fixed-point theorem (monotone endofunctions on a pointed DCPO have a fixed point - no continuity needed) in https://github.com/UniMath/UniMath/blob/master/UniMath/Algebra/FixedPointTheorems.v...

> And what about the prerequisites for that file? See https://github.com/UniMath/UniMath/pull/1726 for a concrete suggestion on this.

> @nmvdw : is this issue solved? Not fully yet. There is still some material that needs to be moved to OrderTheory (partial orders, well-founded sets).