Jason Gross (Feb 28 2023 at 00:04): Jason Gross (Feb 28 2023 at 00:04):It's supposed to be the case that if A <: B and B <: C then A <: C, right?
Jason Gross (Feb 28 2023 at 00:10):(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