`{Funext} : VeryWeakUnivalence -> Univalence_type. Proof. intros vwu. apply WeakUnivalence_implies_Univalence. simple refine (_;_). { intros A B f. refine (unit vwu A @ _ @ (unit vwu B)^). refine (_ @ flip vwu A B (fun a b => f a = b) @ _). - apply ap, path_arrow; intros a. symmetry; rapply (contract vwu). - apply ap, path_arrow; intros b. apply (contract vwu); exact _. } { intros A B f. apply path_equiv, path_arrow; intros a; cbn. rewrite !transport_pp. refine (moveR_transport_V idmap (unit vwu B) _ (f a) _). rewrite !(unit_comp vwu). rewrite <- !(transport_compose idmap sig). rewrite (transport_sigma' (C := fun P (a0:A) => P a0)); cbn. refine (ap _ _ @ _). 1:{ apply ap, ap. exact (path_contr _ (f a ; 1)). } rewrite (flip_comp vwu). rewrite transport_sigma'; cbn. apply ap, path_contr. } Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import Metatheory.Core.