3
$\begingroup$

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").
Improve this question
$\endgroup$
2
  • $\begingroup$ What if you do simple refine (tpair _ _ _) and then refine empty in the first goal? Do either of these give error messages? $\endgroup$
    – Jason Gross
    Commented Apr 20, 2022 at 14:39
  • $\begingroup$ The first one is fine, but the second one gives an error The term "∅" has type "UU" while it is expected to have type "Type" (universe inconsistency: Cannot enforce UU.u0 <= Spartan_exercises.9 because Spartan_exercises.9 < UU.u0). $\endgroup$
    – Tempestas Ludi
    Commented Apr 21, 2022 at 8:14

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
10
  • $\begingroup$ Set Printing Universes does not yield any more information. $\endgroup$
    – Tempestas Ludi
    Commented Apr 21, 2022 at 8:18
  • $\begingroup$ Unset Universe Checking indeed solves my problem when I replace UU by Type. $\endgroup$
    – Tempestas Ludi
    Commented Apr 21, 2022 at 8:21
  • $\begingroup$ Note that the first error is thrown at the line Theorem exercise_1_4: .... This does not yet have anything to do with the universe of fill_me, and indeed, is not solved by having fill_me work on a bigger universe. Also note that in UniMath, UU is defined as UU := Type. $\endgroup$
    – Tempestas Ludi
    Commented Apr 21, 2022 at 8:23
  • $\begingroup$ So would there be a way to solve this without allowing universe inconsistencies (because those would allow for paradoxes)? $\endgroup$
    – Tempestas Ludi
    Commented Apr 21, 2022 at 8:24
  • $\begingroup$ Also, the file UniMath.Foundations.Preamble has on one of the first lines Definition UU := Type. So why is there different behaviour when using UU vs Type? $\endgroup$
    – Tempestas Ludi
    Commented Apr 21, 2022 at 12:00

Not the answer you're looking for? Browse other questions tagged or ask your own question.