Definition dirprod_with_prop' (A B : UU) (isa : isaprop A) : A × B × A ≃ B × A. Proof. intermediate_weq ((A × B) × A). apply invweq, weqtotal2asstor. intermediate_weq (A × (A × B)). apply weqdirprodcomm. intermediate_weq ((A × A) × B). apply invweq, weqtotal2asstor. intermediate_weq (A × B). apply weqdirprodf. - apply dirprod_with_prop; assumption. - apply idweq. - apply weqdirprodcomm. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.