proposition: Lemma funextcontrUAH : funextcontrStatement.
proof: Proof. unfold funextcontrStatement. intros. use (iscontrretract (X := ∏ t, ∑ p, p = g t)). - intros x. use tpair. + intro t. exact (pr1 (x t)). + intro t; simpl. exact (pr2 (x t)). - intros y t. exists (pr1 y t). exact (pr2 y t). - intros u. induction u as [t x]. apply idpath. - apply funcontrUAH. intro t. apply iscontrcoconustot. Defined.
imports: UniMath.Foundations.PartB