`{Funext} {A : Type} (a : A) (P : forall x, (a = x) -> Type) : P a 1 <~> forall x p, P x p := Build_Equiv _ _ (paths_ind a P) _. Global Instance isequiv_paths_ind_r `{Funext} {A : Type} (a : A) (P : forall x, (x = a) -> Type) : IsEquiv (paths_ind_r a P) | 0. Proof. refine (isequiv_adjointify (paths_ind_r a P) (fun f => f a 1) _ _). - intros f. apply path_forall; intros x. apply path_forall; intros p. destruct p; reflexivity. - intros u. reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.