Lemma union_or {X : UU} : ∏ A B : X → hProp, union (λ C : X → hProp, C = A ∨ C = B) = (λ x : X, A x ∨ B x). Proof. intros A B. apply funextfun ; intro x. apply hPropUnivalence. - apply hinhuniv. intros C. generalize (pr1 (pr2 C)). apply hinhfun. apply sumofmaps. + intro e. rewrite <- e. left. apply (pr2 (pr2 C)). + intro e. rewrite <- e. right. apply (pr2 (pr2 C)). - apply hinhfun ; apply sumofmaps ; [ intros Ax | intros Bx]. + exists A. split. * apply hinhpr. now left. * exact Ax. + exists B. split. * apply hinhpr. now right. * exact Bx. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.