## Stream: Coq users

### Topic: Basic universes question

#### Li-yao (Mar 29 2021 at 21:48):

Why does `unfold` or not `unfold`-ing a definition during the following proof set whether or not I get an equality or inequality constraint between universes?

``````Set Printing All.
Set Printing Universes.

Notation set T := (T -> Prop).

Definition set_incl {A} (m1 m2 : set A) :=
forall (a : A), m1 a -> m2 a.

Definition set1 {T} (a : T) : set T := eq a.

Lemma subset_singl :
forall {T} (x y : T), set_incl (set1 x) (set1 y) -> y = x.
Proof.
intros * H.
unfold set1 in H. (* Comment this out *)
apply H. reflexivity.
Qed.

Print Universes Subgraph (eq.u0 set1.u0).
(* yes unfold: set1.u0 <= eq.u0 *)
(* no  unfold: set1.u0  = eq.u0 *)
``````

#### Matthieu Sozeau (Mar 29 2021 at 22:01):

If you don't unfold, the Coq does a successful first-order unification of `set1 y` with `eq y` and that requires that the heads both have the same type, so `forall T : Type@{set1.u0}, T -> T -> Prop` gets unified with `forall T : Type@{eq.u0}, T -> T -> Prop`

#### Matthieu Sozeau (Mar 29 2021 at 22:02):

As we only have equivariant subtyping on the domains of products, you get an equality.

Last updated: Feb 04 2023 at 21:02 UTC