Definition dirprod_with_prop (A : UU) (isa : isaprop A) : A × A ≃ A. Proof. apply weqpr1, iscontraprop1; assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.