Coq introduces a universe constraint `Set < u`

in the definition below and I don't understand why it adds this constraint. Is it not implied by `u0 < u`

(which is the second constraint Coq generates)? Both `u := Prop`

and `u := Set`

suffice to conclude `u >= Set+1`

, AFAICT.

```
Definition type_or_prop@{u u0} (b : bool) : Type@{u} :=
if b then Prop else Type@{u0}.
(* {type_or_prop.u0 type_or_prop.u} |= Set < type_or_prop.u
type_or_prop.u0 < type_or_prop.u *)
```

monomorphic univs are always declared > Set

`u0`

is not > Set, is it?

actually it is, but the implicit > Set is not listed (being implicit)

also Coq does not especially try to remove redundant constraints

Hm. So what decides whether a `> Set`

constraint is implicit or explicit, i.e. printed?

some magic

I recommend not caring

Okay, I'll try to not care about that. :)

Last updated: Jan 29 2023 at 01:02 UTC