{A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) (S : A -> Type) (s0 : S a0) (cp : Contr (pfamMap R S r0 s0)) : exists f : pfamMap R S r0 s0, forall g, pfammap_homotopy f g. Proof. snrefine (_;_). - exact (@center _ cp). - intro g. by destruct (@contr _ cp g). Defined.
Require Import Basics. Require Import Types.Sigma Types.Equiv Types.Paths. Require Import HoTT.Tactics.