proposition: Theorem QInv_Univalence_implies_FunextNondep (A B : Type) : forall f g : A -> B, f == g -> f = g.
proof: Proof. intros f g p. pose (d := fun x : A => exist (fun xy => fst xy = snd xy) (f x, f x) (idpath (f x))). pose (e := fun x : A => exist (fun xy => fst xy = snd xy) (f x, g x) (p x)). change f with ((snd o pr1) o d). change g with ((snd o pr1) o e). rapply (ap (fun g => snd o pr1 o g)). pose (fun A B x y=> @equiv_inv _ _ _ (@isequiv_ap _ _ _ (@isequiv_src_compose A B) x y)) as H'. apply H'. reflexivity. Defined.
imports: HoTT(Basics Types HProp HSet Projective TruncType Truncations Modalities.Notnot Modalities.Open Modalities.Closed BoundedSearch Equiv.BiInv Spaces.Nat Spaces.Torus.TorusEquivCircles Metatheory.Core Metatheory.FunextVarieties)