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 *)
```

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`

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

Last updated: Sep 28 2023 at 10:01 UTC