{A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) (H : forall S : A -> Type, forall s0 : S a0, exists f : pfamMap R S r0 s0, forall g, pfammap_homotopy f g) (a : A) : IsEquiv (fun p : a0 = a => transport R p r0). Proof. pose (inv := (H (fun a => a0 = a) 1).1.1). pose proof (inv_beta := (H (fun a => a0 = a) 1).1.2); cbn in inv_beta. snrapply (isequiv_adjointify _ (inv a)); cbn. - destruct (H R r0) as [[f fp] h]. pose proof (h' := fun g => (h g).1 a); cbn in h'; clear h fp. transitivity (f a). + symmetry. nrefine (h' (fun _ _ => transport R (inv _ _) r0; _)). exact (ap (fun x => transport R x r0) inv_beta). + exact (h' (_; idpath)). - by intros []. Defined.
Require Import Basics. Require Import Types.Sigma Types.Equiv Types.Paths. Require Import HoTT.Tactics.