Niels van der Weide

Yes. The easiest change is to move https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/WellOrderedSets.v and https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/OrderedSets.v, and a more complicated change would be to move the stuff on posets.

I think both.

> Constants relying on "type in type" are printed by [Print Assumptions](https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Print-Assumptions). I think this is a big upside. This way it is easier to detect what precisely relies on...

> Right, I just tested the change and it will definitely disable universe checking for any project using UniMath that today have universe checking enabled, and it will do so...

> > > Constants relying on "type in type" are printed by [Print Assumptions](https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Print-Assumptions). > > > > > > I think this is a big upside. This way it...

To explain my statement. If I make the following file: ```coq Definition identity {A : Type} (a : A) := a. Unset Universe Checking. Definition selfid := identity (@identity). ```...

Maybe relevant info: I don't get this error on Mac OS (so, it might be Debian related).

They do not compile the bicategories package due to memory consumption (so, I dunno whether they can pay much attention to it). My guess that in both cases the error...

> Re the axiom — my bad, I thought we’d changed the policy on such admits. I’ll change it to a local assumption. > > (I thought we’d changed the...

In `Bicategories/Core/Bicat.v`, removing `#[local] Unset Universe Checking.` would give an error at this line: ```coq Definition prebicat_2cell_struct (C : precategory_ob_mor) : UU := ∏ (a b: C), C⟦a, b⟧ →...