NaiveNondepFunext. Proof. intros A B 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.
Require Import HoTT.Basics. Require Import Types.Universe. Require Import Metatheory.Core Metatheory.FunextVarieties.