NaiveFunext_implies_WeakFunext@{i j max} : NaiveFunext@{i j max} -> WeakFunext@{i j max}. Proof. intros nf A P Pc. apply (Build_Contr _ (fun x => center (P x))). intros f; apply nf; intros x. apply contr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Metatheory.Core.