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").
$\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$ Apr 20 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$ Apr 21 at 8:14

1 Answer 1

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.

$\endgroup$
10
  • $\begingroup$ Set Printing Universes does not yield any more information. $\endgroup$ Apr 21 at 8:18
  • $\begingroup$ Unset Universe Checking indeed solves my problem when I replace UU by Type. $\endgroup$ Apr 21 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$ Apr 21 at 8:23
  • $\begingroup$ So would there be a way to solve this without allowing universe inconsistencies (because those would allow for paradoxes)? $\endgroup$ Apr 21 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$ Apr 21 at 12:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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