NaiveFunext_implies_NaiveNondepFunext@{i j max} : NaiveFunext@{i j max} -> NaiveNondepFunext@{i j max} := fun nf A B f g => nf A (fun _ => B) f g. Section Homotopies. Context (wf : WeakFunext). Context {A:Type} {B : A -> Type}. Context (f : forall x, B x). Let idhtpy : f == f := fun x => idpath (f x). Global Instance contr_basedhtpy : Contr {g : forall x, B x & f == g } | 1. Proof. unfold WeakFunext in wf. apply (Build_Contr _ (f;idhtpy)). intros [g h]. pose (r := fun k => exist (fun g => f == g) (fun x => (k x).1) (fun x => (k x).2)). pose (s := fun (g : forall x, B x) (h : f == g) x => (g x ; h x)). change (r (fun x => (f x ; idpath (f x))) = r (s g h)). apply ap; srapply path_contr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Metatheory.Core.