NaiveNondepFunext_implies_Funext@{i j max} : NaiveNondepFunext@{i max max} -> Funext_type@{i j max} := WeakFunext_implies_Funext o NaiveNondepFunext_implies_WeakFunext.
Require Import HoTT.Basics HoTT.Types. Require Import Metatheory.Core.