Lemma dirprod_with_contr_r : ∏ X Y : UU, iscontr X -> (Y ≃ Y × X). Proof. intros X Y iscontrX. intermediate_weq (Y × unit); [apply weqtodirprodwithunit|]. - apply weqdirprodf. * apply idweq. * apply invweq, weqcontrtounit; assumption. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartB.