Skip to main content
Proof Assistants Beta

Return to Answer

Explain actual universe error at the theorem statement rather than the exact
Source Link
Jason Gross
Jason Gross
  • 1.5k
  • 4
  • 11

This is a universe inconsistency. You might get slightly more details with Set Printing Universes.. The type fill_me∑ axiom allows filling anyis defined in Preamble.v to take its first argument as a type in in the universe UUUU. The type Hence ∑ A:UU, (A → empty) does not live in UU, for the same reason thattypecheck because UU doesis not livea 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 puttingreplacing fill_meUU with Type. However, as empty is in UU and not a potentially largerstrictly smaller universe, for exampleyou cannot refine with Axiom fill_me : forall {Xtpair :_ Type},empty X._ 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.

This is a universe inconsistency. You might get slightly more details with Set Printing Universes.. The fill_me axiom allows filling any type in the universe UU. The type ∑ A:UU, (A → empty) does not live in UU, for the same reason that UU does not live 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 by putting fill_me in a potentially larger universe, for example Axiom fill_me : forall {X : Type}, X.. 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.

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.

Source Link
Jason Gross
Jason Gross
  • 1.5k
  • 4
  • 11

This is a universe inconsistency. You might get slightly more details with Set Printing Universes.. The fill_me axiom allows filling any type in the universe UU. The type ∑ A:UU, (A → empty) does not live in UU, for the same reason that UU does not live 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 by putting fill_me in a potentially larger universe, for example Axiom fill_me : forall {X : Type}, X.. 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.