WeakUnivalence -> Univalence_type. Proof. intros [etop H] A. apply isequiv_from_functor_sigma. srapply isequiv_contr_contr. srapply (contr_retracttype (Build_RetractOf _ _ (fun Be => (Be.1 ; equiv_path A Be.1 Be.2)) (fun Bf => (Bf.1 ; etop A Bf.1 Bf.2)) _)). intros [B f]. refine (path_sigma' (fun B => A <~> B) 1 (H A B f)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import Metatheory.Core.