Found type UU where "?T" was expected

Question

I am trying to solve a couple of exercises in coq. However, with the following code:

Require Import UniMath.Foundations.PartD.

(** The following axiom allows us to inhabit any type.
    It is a way of indicating where you need to fill in
    your own solutions. Remove it once you're done with
    all the exercises. *)
Axiom fill_me : forall {X : UU}, X.

Theorem exercise_1_4 : ∑ A:UU, (A → empty).
Proof.
   exact fill_me.
Qed.

I get the error Found type "UU" where "?T" was expected at the line of the theorem statement. I can replace UU by Type (which is definitionally equal, I believe), which allows me to start writing the proof, but then using refine (tpair _ empty _). in the proof gives the following (even more impressive-looking) error:

The term "∅" has type "UU" while it is expected to have type 
"?T" (unable to find a well-typed instantiation for 
"?T": cannot ensure that "Type" is a subtype of "UU").

Answer 1

This is a universe inconsistency. You might get slightly more details with Set Printing Universes.. The type ∑ is defined in Preamble.v to take its first argument as a type in UU. Hence ∑ A:UU, (A → empty) does not typecheck because UU is not a type in UU. You can fix this error either by doing Unset Universe Checking (the equivalent of UniMath's -type-in-type flag that is globally passed), or, as you note, by replacing UU with Type. However, as empty is in UU and not a strictly smaller universe, you cannot refine with tpair _ empty _ without hitting the same universe inconsistency. Note that Unset Universe Checking allows proofs of False (but they are relatively hard to find, which is why UniMath gets away with ignoring universe checking). The more-confusing error message on refine probably comes from mixing record types defined with -type-in-type with code where universes are checked.