WeakFunext_implies_Funext@{i j max} : WeakFunext@{i j max} -> Funext_type@{i j max}. Proof. intros wf; hnf; intros A B f g. refine (isequiv_adjointify (@apD10 A B f g) (htpy_ind wf f (fun g' _ => f = g') idpath g) _ _). - revert g; refine (htpy_ind wf _ _ _). refine (ap _ (htpy_ind_beta wf _ _ _)). - intros h; destruct h. refine (htpy_ind_beta wf _ _ _). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Metatheory.Core.