fact: Definition binary_intersection' {X : UU} (U V : hsubtype X) : hsubtype X := subtype_intersection (λ b, bool_rect (λ _ : bool, hsubtype X) U V b).
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions