`{Univalence} : DProp <~> Bool := Build_Equiv _ _ dprop_to_bool _.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HProp. Require Import Truncations.Core Modalities.ReflectiveSubuniverse.