proposition: Lemma union_or {X : UU} : ∏ A B : X → hProp, union (λ C : X → hProp, C = A ∨ C = B) = (λ x : X, A x ∨ B x).
proof: 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.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.FiniteSequences UniMath.Foundations.NaturalNumbers UniMath.Tactics.EnsureStructuredProofs