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