`{Funext} {A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) (S : A -> Type) (s0 : S a0) (fH : exists f : pfamMap R S r0 s0, forall g, pfammap_homotopy f g) : Contr (pfamMap R S r0 s0). Proof. snrapply Build_Contr. - exact fH.1. - intro g. snrapply path_sigma; cbn. + funext a. nrapply path_forall. exact ((fH.2 g).1 a). + transport_path_forall_hammer. lhs nrapply transport_paths_l. nrapply moveR_Vp. nrapply moveL_pM. symmetry. exact (fH.2 g).2. Defined.
Require Import Basics. Require Import Types.Sigma Types.Equiv Types.Paths. Require Import HoTT.Tactics.