(b1 b2 : DHProp) : DHProp := Build_DHProp (Build_HProp (hor b1 b2)) _.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HProp. Require Import Truncations.Core Modalities.ReflectiveSubuniverse.