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").

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").

I am working on 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").

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").