proposition: Theorem WeakUnivalence_implies_Univalence : WeakUnivalence -> Univalence_type.
proof: 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.
imports: HoTT.Basics HoTT.Types Idempotents Metatheory.Core