It's supposed to be the case that if `A <: B`

and `B <: C`

then `A <: C`

, right?

(It's currently not the case, and has not been the case at least since Coq 8.4:

```
Module Type C. Axiom t : Type. Axiom a : @id Type t. End C.
Module Type B <: C. Axiom t : Type. Axiom a : t. End B.
Module Type A <: B. Axiom t : Set. Axiom a : @id Set t. End A.
Module Type A' <: B := A.
Module Type A'' <: B <: C := A.
(* Error: Universe inconsistency. Cannot enforce Set = foo.2 because foo.2 < foo.1
<= foo.2 = Set.
*)
```

)

Last updated: Sep 15 2024 at 13:02 UTC