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