`{Contr A} `(P : A -> Type) : (forall a, P a) <~> P (center A). Proof. simple refine (equiv_adjointify (fun (f:forall a, P a) => f (center A)) _ _ _). - intros p a; exact (transport P (path_contr _ _) p). - intros p. refine (transport2 P (q := 1) _ p). apply path_contr. - intros f; apply path_forall; intros a. apply apD. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids