proposition: Lemma union : forall v, hexists (fun w => forall x, x ∈ w <-> hexists (fun u => x ∈ u * u ∈ v)).
proof: Proof. intro v. apply tr; exists (V_union v). intro x; split. - intro H. simpl in H. generalize H; apply (Trunc_functor (-1)). intros [[u' x'] p]; simpl in p. exists (func_of_members u'); split. + refine (transport (fun z => x ∈ z) (is_valid_presentation (func_of_members u'))^ _). simpl. apply tr; exists x'. exact p. + refine (transport (fun z => func_of_members u' ∈ z) (is_valid_presentation v)^ _). simpl. apply tr; exists u'; reflexivity. - apply Trunc_rec. intros [u (Hx, Hu)]. generalize (transport (fun z => u ∈ z) (is_valid_presentation v) Hu). apply Trunc_rec. intros [u' pu]. generalize (transport (fun z => x ∈ z) (is_valid_presentation (func_of_members u')) (transport (fun z => x ∈ z) pu^ Hx)). apply Trunc_rec. intros [x' px]. apply tr. exists (u'; x'). exact px. Qed.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient