Lemma maponsec1l2 {X : UU} (P : X -> UU) (f : X -> X) (h : ∏ x, f x = x) (s : ∏ x, P x) x : maponsec1l0 P f h s x = s x. Proof. intros. set (map := λ (ff : (∑ (f0 : X -> X), ∏ x, (f0 x) = x)), maponsec1l0 P (pr1 ff) (pr2 ff) s x). assert (is1 : iscontr (∑ (f0 : X -> X), ∏ x, (f0 x) = x)) by apply funextcontr. assert (e: (f,,h) = tpair (λ g, ∏ x, g x = x) (λ x, x) idpath) by (apply proofirrelevancecontr; assumption). apply (maponpaths map e). Defined.