`{Funext} `{P : A -> Type} `{forall a, Contr (P a)} : Contr (forall a, P a). Proof. apply (Build_Contr _ (fun a => center (P a))). intro f. apply path_forall. intro a. apply contr. Defined.
Require Import