proposition: Theorem IncoherentWeakUnivalence_implies_Univalence `{Funext} : IncoherentWeakUnivalence -> Univalence_type.
proof: 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.
imports: HoTT.Basics HoTT.Types Idempotents Metatheory.Core