Univalence_type -> WeakFunext := NaiveNondepFunext_implies_WeakFunext o @Univalence_implies_FunextNondep.
Require Import HoTT.Basics. Require Import Types.Universe. Require Import Metatheory.Core Metatheory.FunextVarieties.