`{Funext} {A : pType} {P : pFam A} (f g : pForall A P) : (f ==* g) <~> (f = g). Proof. refine (_ oE (issig_phomotopy f g)^-1). revert f g; apply (equiv_path_issig_contr (issig_pforall A P)). { intros [f feq]; cbn. exists (fun a => 1%path). exact (concat_pV _)^. } intros [f feq]; cbn. contr_sigsig f (fun a:A => idpath (f a)); cbn. refine (contr_equiv' {feq' : f (point A) = dpoint P & feq = feq'} _). refine (equiv_functor_sigma' (equiv_idmap _) _); intros p. refine (_^-1 oE equiv_path_inverse _ _). apply equiv_moveR_1M. Defined.
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.