fact: Definition path_dhprop `{Univalence} {P Q : DHProp} : (P = Q :> Type) -> (P = Q :> DHProp) := equiv_path_dhprop P Q.
imports: HoTT.Basics HoTT.Types TruncType HProp Truncations.Core Modalities.ReflectiveSubuniverse