`{Funext} : IncoherentWeakUnivalence -> Univalence_type. Proof. intros [etop K]. apply WeakUnivalence_implies_Univalence. transparent assert (etop' : (forall A B, (A <~> B) -> (A = B))). { intros A B f. refine (etop A B f f^-1 _ _). - intros x; apply eisretr. - intros x; apply eissect. } exists etop'. intros A B f. apply path_equiv, path_arrow, K. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import Metatheory.Core.