Definition constr1 {X : UU} (P : X -> UU) {x x' : X} (e : x = x') : ∑ (f : P x -> P x'), ∑ (ee : ∏ p : P x, tpair _ x p = tpair _ x' (f p)), ∏ (pp : P x), maponpaths pr1 (ee pp) = e. Proof. intros. induction e. split with (idfun (P x)). split with (λ p, idpath _). unfold maponpaths. simpl. intro. apply idpath. Defined.