NaiveNondepFunext -> WeakFunext. Proof. intros nf X P H. pose (T := (hfiber (equiv_postcompose_from_NaiveNondepFunext nf (equiv_pr1 P)) idmap)). exact (@contr_retract T _ _ (fun fp x => transport P (ap10 fp.2 x) (fp.1 x).2) (fun f => ((fun x => (x ; f x)) ; 1)) (fun f => 1)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Metatheory.Core.