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: Dec 05 2023 at 05:01 UTC