Lemma union_hfalse {X : UU} : union (λ _ : X → hProp, hfalse) = (λ _ : X, hfalse). Proof. apply funextfun ; intros x. apply hPropUnivalence. - apply hinhuniv. intros A. apply (pr1 (pr2 A)). - apply fromempty. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.