fact: Definition Univalence_implies_WeakFunext : Univalence_type -> WeakFunext := NaiveNondepFunext_implies_WeakFunext o @Univalence_implies_FunextNondep.
imports: HoTT.Basics Types.Universe Metatheory.Core Metatheory.FunextVarieties