Lemma dirprod_with_contr_l : ∏ X Y : UU, iscontr X -> (Y ≃ X × Y). Proof. intros X Y iscontrX. intermediate_weq (Y × X). - apply dirprod_with_contr_r; assumption. - apply weqdirprodcomm. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartB.