Funext_implies_NaiveFunext@{i j max} : Funext_type@{i j max} -> NaiveFunext@{i j max}. Proof. intros fe A P f g h. unfold Funext_type in *. exact ((@apD10 A P f g)^-1 h). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Metatheory.Core.