proposition: Lemma equiv_hprop_idprod `{Univalence} (A : Type) (P : Type) (a : merely A) `{IsHProp P} : P <-> (P * A = A).
proof: Proof. split. - intros p; apply path_universe with snd. apply isequiv_adjointify with (fun a => (p,a)). + intros x; reflexivity. + intros [p' x]. apply path_prod; [ apply path_ishprop | reflexivity ]. - intros q. strip_truncations. apply equiv_path in q. exact (fst (q^-1 a)). Defined.
imports: Basics Types HoTT.Truncations Spaces.BAut Spaces.BAut.Rigid ExcludedMiddle